The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Kenneth Roe wrote:
> Notice the introduction of "@existT".

Your post has way too much code for me to digest.  However, if all 
you're asking is how to apply injectivity on equalities between [existT] 
terms, then see:
    Require Import Eqdep.
    Check inj_pair2.

Note that [inj_pair2] relies on an axiom.  I often go to some trouble to 
avoid depending on such axioms, but your proof state is already too far 
along to be saved by such tricks.  If you happen to have decidable 
equality on the appropriate type, then you can instead use the following 
axiom-free:
    Require Import Eqdep_dec.
    Check inj_pair2_eq_dec.

Otherwise, see Section 12.3.4 of CPDT for a discussion of the issue.  If 
you don't mind axioms, then the [crush] tactic of CPDT will do 
everything you want, as it automatically applies [inj_pair2], among many 
other common proof steps.