The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

roconnor AT theorem.ca
 wrote:
> We can prove something more general.
>
> Require Import Eqdep_dec.
> Lemma l1 : forall x : T 0, T0 = x.
> intros n.
> change (T0) with (eq_rec 0 T T0 0 (refl_equal 0)).
> generalize (refl_equal 0).
> revert n.
> set (z:=0).
> unfold z at 2 5.
> generalize z.
> clear z.
> intros z [] e.
> pattern e.
> apply (K_dec).
>  intros x y.
>  destruct (eq_nat_dec x y); auto.
> reflexivity.
> Qed.
>
> Maybe more clever Coq people know how to make a shorter proof.

Here's how I would do it, without using any of the tactics I've 
developed over the years for simplifying this sort of thing:

Require Import Eqdep.

Inductive T : nat -> Set := T0 : T 0.

Notation "e :? pf" := (eq_rect _ (fun X : Set => X) e _ pf)
 (no associativity, at level 90).

Lemma l1' : forall n (x : T n) Heq, T0 = (x :? Heq).
 destruct x; intro Heq; rewrite (UIP_refl _ _ Heq); reflexivity.
Qed.

Lemma l1 : forall x : T 0, T0 = x.
 intros; change x with (x :? refl_equal _); apply l1'.
Qed.