The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Ondrej Rypacek wrote:
> is it possible to prove the following in Coq?
>
> Inductive X : nat -> Set := XZero : X 0.
>
> Lemma Xinv: forall (x:X 0), x = XZero.

Ironically, the subject of your message answers the question (sort of). :)

Require Import Program.

Lemma Xinv: forall (x:X 0), x = XZero.
  dependent induction x; reflexivity.
Qed.

In fact, no inductive hypothesis is needed here, so you could use 
[dependent destruction] instead.

These tactics will sometimes appeal to axioms.  Your example has an easy 
axiom-free proof, though.

Definition Xinv' : forall (x:X 0), x = XZero :=
  fun x => match x as x in X n return match n return X n -> Prop with
                                        | O => fun x => x = XZero
                                        | _ => fun _ => True
                                      end x with
             | XZero => refl_equal _
           end.