The Coq mailing list

[t x <txrev319 AT gmail.com>]

Consider the following code block:

Inductive Nat : Type :=
| O: Nat
| S: forall (n: Nat), Nat.

Lemma lem:
  O <> S O.
Proof.
  intro H.
  inversion H. Qed.

Print lem.

(*

Is there a simpler proof of this?


lem = 
fun H : O = S O =>
(fun H0 : S O = S O -> False => H0 eq_refl)
  match H in (_ = y) return (y = S O -> False) with
  | eq_refl =>
      fun H0 : O = S O =>
      (fun H1 : O = S O =>
       (fun H2 : False => (fun H3 : False => False_ind False H3) H2)
         (eq_ind O
            (fun e : Nat => match e with
                            | O => True
                            | S _ => False
                            end) I (S O) H1)) H0
  end
     : O <> S O


*)

I don't find this particularly insightful.
Is there a shorter manually written proof?