The Coq mailing list

[Ondrej Rypacek <oxr AT Cs.Nott.AC.UK>]

Dear all,
is it possible to prove the following in Coq?

Inductive X : nat -> Set := XZero : X 0.

Lemma Xinv: forall (x:X 0), x = XZero.


Inversion makes no progress; case analysis on x results in an ill-typed 
term:

Error: Abstracting over the terms "0" and "x" leads to a term
"fun (n : nat) (x : X n) => x = XZero" which is ill-typed.


Am I right to assume that this is a case for heterogeneous (J.M.) 
equality as I would like to conclude that (x : X n = XZero : X 0) ? But 
will I be able to obtain Xinv from that?

Many thanks in advance for any pointers !
Regards,
Ondrej