The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

Can the following lemma be proven in Coq:?

Lemma eq_sigS : (A:Set; P:(A -> Set); x:A; e,e':(P x))
                (existS A P x e)=(existS A P x e') -> e=e'.

I can start out with the following tactics,

Intros.
Replace e with (projS2 A P (existS A P x e)).

And then try "Rewrite H", which results in "Error: Cannot solve a 
second-order unification problem".

Thanks for any help,

--- nadeem

-------------------
To unsubscribe, mail 
coq-club-request AT pauillac.inria.fr
Bug reports: http://coq.inria.fr/bin/coq-bugs
Coq-Club Archives: http://coq.inria.fr/mailing-lists/coqclub/