The Coq mailing list

[Geoff Reedy <geoff AT programmer-monk.net>]

On Thu, Oct 10, 2013 at 01:16:53PM -0700, t x said
> Inductive Nat : Type :=
> | O: Nat
> | S: forall (n: Nat), Nat.
> 
> Lemma lem:
>   O <> S O.
> [...]
> Is there a simpler proof of this?

I think this is as short as it gets:

eq_ind O (fun n => match n with O => True | S _ => False end) I (S O)