The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

In the following example, is use of proof_irrelevance necessary?  Is 
there some way to avoid its use when the domain of the predicate 
involved is nat, for example?

Thanks in advance.  -- Sam


Require Import Arith.
Require Import ProofIrrelevance.

Variable n : nat.

Definition t := sig (fun i => i < n).

Definition f (x : t) : sig (fun i => i < S n).
  intros [i Hi].
  refine (exist _ (S i) _).
  auto with arith.
Defined.

Lemma lem : forall x y, f x = f y -> x = y.
  intros [x Hx] [y Hy] Heq.
  injection Heq as Heq'.
  clear Heq.
  revert Hx Hy; rewrite Heq'; intros Hx Hy.
  rewrite (proof_irrelevance _ Hx Hy).
  reflexivity.
Qed.