The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Mon, Jan 10, 2005 at 10:39:35PM -0500, Robert Dockins wrote:

> I can easily get to where I have a assumption that seems like it
> should lead to a contradiction, but I can't tease it out.  The form
> of it is:

> H: x = TermIf TermTrue x y

> It seams clear that such an x cannot exist as term is defined with
> Inductive, but how do I make the proof go through?  Have I made some
> miskake?

This property can be proven by induction:

Lemma Foo: forall x y:term, x <> TermIf TermTrue x y.
Proof.
intro x; induction x; intros; try discriminate.
injection.
intros.
apply (IHx2 x3).
rewrite <- H2.
exact H1.
Qed.

-- 
Lionel