The Coq mailing list

[bertot <(e29315a54f%hidden_head%e29315a54f)Yves.Bertot(e29315a54f%hidden_at%e29315a54f)inria.fr(e29315a54f%hidden_end%e29315a54f)>]

Dear all,

I have unclear memories of formal proofs that proofs of comparison (not 
equalities) are unique.  More precisely, proofs of the following 
proposition:

forall n m, forall h1 h2 : le n m,  h1 = h2

Could someone point me to one such development?  It seems the 
developments by Cédric Auger and Matthieu Sozeau in an answer to a 
question by Pierre Castéran on proofs of finiteness of streams is 
related, but I have not been able to understand it enough to transpose 
it to the other question.

Yves