■

combine_splitが分からん。
証明は出来た。しかしどやってdestructを使うのか分からねえ。

Theorem split_fst_snd : forall (X Y: Type) ( l : list (X * Y)),
 split l = ((fst (split l)), (snd (split l))).
Proof.
 intros. induction l as [| [x y] l'].
 simpl.  reflexivity.
 simpl.
 reflexivity.
Qed.
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
  split l  = (l1, l2) ->
  combine l1 l2 = l. 
Proof.
  intros X Y l. induction l as [| [x y] l']. (* この書き方も謎だ *)
  Case "l=nil".
  intros l1 l2 H. simpl in H.
  inversion H. reflexivity.
  Case "(x, y) :: l".
  intros l1 l2 H.  simpl in H.
  inversion H.  simpl.  
  assert(H3: combine (fst (split l')) (snd (split l')) = l').
  apply IHl'. rewrite <- split_fst_snd. reflexivity. rewrite H3. reflexivity.
Qed.
(*destructでてこねえ*)

• • -

よめはんの体調は順調のようだ。よかったよかった。
トキソプラズマの可能性ありとか言われてるようだけど、まあだいじょぶでしょう。