The Coq mailing list

[t x <txrev319 AT gmail.com>]

Vincent, Robbert, Geoff: your examples are much more insightful.

I particularly like Robbert's example. It has just the right amount of "generalizable to other cases" + "simple to understand."

Thanks!

On Thu, Oct 10, 2013 at 1:43 PM, Geoff Reedy <geoff AT programmer-monk.net> wrote:

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)