The Coq mailing list

[Fr�d�ric Gava <frederic.gava AT wanadoo.fr>]

Dear users,

 

For the first Lemma, I just forget to siomplify my sub-goals...

just do:

 

Lemma put_tmp2: (T:Set)(l1,l2:(list Z->(option T)))(l:(list Z->(option T)))(i,j:Z)
                (Zlength (Z->(option T)) (put_tmp T l1 i l))=(Zlength (Z->(option T))(put_tmp T l2 j l)).

Intros T l.

NewInduction l;Simpl; Intros; Auto.

Rewrite (IHl l1 l2 `i+1` `j+1`); Auto.

Qed

 

Sorry for this stupid question but I do not have the proof for my second function (the Double Induction tactics does not work here).

 

best regards,

Frédéric Gava