The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

mulhern wrote:
> Is there a general way to ignore proofs when deciding equality...or is
> my current approach actually necessary?

If you are willing to tolerate an axiom, then the Eqdep module of the 
standard library provides proof irrelevance for equality:
        http://coq.inria.fr/library/Coq.Logic.Eqdep.html

That is, its UIP lemma uses the axiom to show that any two proofs of the 
same equality fact are equal.  You can use the lemma in justifying the 
correctness of equality decision procedures that ignore proof components.