The Coq mailing list

[GANGCHEN5 AT aol.com]

Hello,

Given an inductive definition:

Inductive A : Set := a : A | b : A | c : A.

I want to prove that each pair of two constructors are
different. Here is a proof following the method proposed in the book CoqArt:

Lemma ineq : ~a=b.
Proof.
Unfold not; Intros H; Change ([o:A]Cases o of a => True | _ => False end b);Rewrite <- H; Trivial.
Qed.

Question:
Are there simpler or general proofs for this problem ?

With the above method, each lemma ~x=y needs a slightly different proof.


Thanks.

gang chen