The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Stéphane Glondu wrote:
>> 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?
> 
> In that particular case, there might be. See the "Proof irrelevance for
> le" thread in the archives of this mailing-list.

More specifically, the following works after pasting it after Pierre
Letouzey's code from:

  http://pauillac.inria.fr/pipermail/coq-club/2008/004030.html

--8<------------------------------------------------------------
Lemma lt_eq : forall x y (H1 H2: x < y), H1 = H2.
Proof.
  intros.
  hnf in *.
  rewrite (le_eq _ _ H1 H2).
  reflexivity.
Qed.

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 (lt_eq _ _ Hx Hy).
  reflexivity.
Qed.
--8<------------------------------------------------------------

Cheers,

-- 
Stéphane Glondu