The Coq mailing list

[Ramon <i AT ramon.org.il>]

Hello,

I am playing around with Coq, and got stuck when trying to prove:

Lemma existT_equal
    : forall T F (X : T) a b,
        existT F X a = existT F X b ->
            a = b.

Using both apply and eapply using f_equal and projT2 gives type errors, I'm 
guessing that this would require something a bit less straight-forward.

I have attempted many variations of the following, which I understand why is 
wrong, but haven't found a better solution):

eapply f_equal with (f := fun x => projT2 x) in H.

Thanks!