The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Please, see Lemma le_unique in http://color.loria.fr/, module 
Util/Nat/NatUtil.v.

Julien Forest a écrit :
> Dear all, 
> I wonder if one can manage to show proof irrelevance for le without
> using any axiom nor importing ProofIrrelevance library. 
>
> At least, I want to be able to show that le is ProofIrrelevant enough
> to be changed in the exist construtor. 
>
>
> Julien
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club