coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof irrelevance for Z.le

From: Thomas Braibant <thomas.braibant AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Proof irrelevance for Z.le
Date: Tue, 31 Jul 2012 14:33:11 -0400

Hi list,

I wonder if there is a way to prove proof-irrelevance for Z.le,
without using the proof-irrelevance axiom?

Lemma proof_irrelevance_Zle n m : forall (p q : Z.le n m), p = q.

Cheers,
Thomas

[Coq-Club] Proof irrelevance for Z.le, Thomas Braibant, 07/31/2012
- Re: [Coq-Club] Proof irrelevance for Z.le, Jason Gross, 07/31/2012
- Re: [Coq-Club] Proof irrelevance for Z.le, Daniel Schepler, 07/31/2012
  - Re: [Coq-Club] Proof irrelevance for Z.le, Thomas Braibant, 07/31/2012