The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Speaking of proof irrelevance for le...   I have a suggestion for an
improved solution to http://coq.inria.fr/faq entry 138.

Require Import Eqdep_dec.
Require Import Eqdep.
Require Import Arith.

Scheme le_ind' := Induction for le Sort Prop.

Lemma le_uniqueness : forall (m n:nat) (le1 le2 : m <= n), le1 = le2.
Proof.
cut (forall (m n:nat) (le1 : m <= n) (n':nat) (le2 : m <= n'),
  n = n' -> eq_dep _ (le m) n le1 n' le2).
intros.
apply eq_dep_eq_dec.
exact eq_nat_dec.
apply H; trivial.

induction le1 using le_ind'; destruct le2.
  constructor.

  intro.
  contradict le2.
  subst.
  apply le_Sn_n.

  intro.
  clear IHle1; contradict le1.
  subst.
  apply le_Sn_n.

  injection 1.
  intro.
  apply IHle1 with (le2 := le2) in H0.
  destruct H0.
  constructor.
Qed.

Print Assumptions le_uniqueness.  (* Closed under the global context *)

(Here I've tried to stick to simple tactics instead of doing what I'd
usually do and combining them more.)
-- 
Daniel Schepler