The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

Hi again,

Given any inductive type, let's say a `nat`-like structure:

Inductive T :=
  |  Zero : T
  |  Succ : T -> T.

I'm in the position where I have to prove that:

Goal forall t: T, t <> Succ t.

If I have to do it the same way as `nat` (e.g. define `eq_nat` and
prove its equivalence with `eq`), it will be quite tedious for my
somewhat larger structures.

This should be trivial for all inductive types, shouldn't it? Is there
an easier way?

Thanks!

--
www.mhelvens.net