The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 07/15/2013 08:59 AM, Michiel Helvensteijn wrote:
> 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.
>    

Generally this work is easy to push off onto [congruence], which is a 
complete decision procedure for equality with constructors.

Goal forall t: T, t <> Succ t.
  induction t; congruence.
Qed.