The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Thank you for the prompt and instructive answer. 
But my understanding is still partial :(

The following code works fine: 

Inductive list: Prop :=
| nil: nat -> list.

Inductive list_eq: list -> list -> Prop :=
| nil_eq: forall n, list_eq (nil n) (nil n).

Lemma invert_again: forall l0 l1, list_eq l0 l1 -> l1 = l0.
Proof.
inversion 1; reflexivity.
Qed.

I do not know where is the crucial difference in proof terms of your "invert"
and my "invert_again".

Best,
Keiko