The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi, 
 
> Lemma apply_tmp_tmp: (A,B:Set) (l1:(list A->B)) (l2:(list A)) 
>     {`(Zlength B (apply_tmp A B l1 l2))=(Zlength A l2)`}+{`(Zlength B 
> (apply_tmp A B l1 l2))=(Zlength [(A->B)] l1)`}.
> Intros.
> 
> 
> Double Induction l1 l2.
> Error: No hypothesis l1 in current goal even after head-reduction
> 
> How prove it ????

  "Double Induction l1 l2" expects l1 and l2 being quantified in the
goal. Just remove your "Intros".

  Anyway, Double Induction is usually too strong for most of
needs. "NewInduction l1; NewDestruct l2" is usually enough (see
section 8.7.4 on Double Induction in the reference manual).

  Regards,

  Hugo