The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 10/10/2013 10:16 PM, t x wrote:
> I don't find this particularly insightful.
> Is there a shorter manually written proof?
The inversion tactic is neither known to generate short nor insightful 
proofs.

Do you like this proof better:

  Definition tx (H : 0 = S 0) : False :=
    match H in eq _ y return
      match y with 0 => True | S _ => False end
    with eq_refl => I end.

It shows it is just a dependent pattern match on an impossible equality 
proof. Recent versions of Coq even accept it without return annotations.

  Definition tx (H : 0 = S 0) : False :=
    match H with eq_refl => I end.