The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You can do it with [functional_extensionality_dep]:

Require Import ZArith.

Require Import FunctionalExtensionality.

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

  compute in *; intros;

    apply functional_extensionality_dep; intro x; contradict x; trivial.

Qed.

I don't know how to do it without functional extensionality; [compute] tells me that, if I try to work by induction, I need to prove [forall p q : (Eq = Gt -> False), p = q].

-Jason

On Tue, Jul 31, 2012 at 2:33 PM, Thomas Braibant <thomas.braibant AT gmail.com> wrote:

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