The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

I've stumped myself again.  I've run into a pretty simple theorem that I
can't figure out how to prove.  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?

Many thanks, code follows.

------------------------

Section TaPLUntypedBools.

Inductive term : Set :=
  | TermTrue : term
  | TermFalse : term
  | TermIf : term -> term -> term -> term.

Reserved Notation "A --> B"  (at level 40, left associativity).

Inductive smallStep : term -> term -> Prop :=
   | EIfTrue  : forall (x y:term),   (TermIf TermTrue x y) --> x
   | EIfFalse : forall (x y:term),   (TermIf TermFalse x y) --> y
   | EIf      : forall (a b x y:term), (a --> b) -> (TermIf a x y) -->
(TermIf b x y)
 where "A --> B" := (smallStep A B).

Lemma SmallStepAntiReflexive : forall t:term, ~(t --> t).
Proof.
intros.
red in |- *.
intro H.
induction t.
 inversion H.
 inversion H.
 inversion H.

(*???? what's next? *)

End TaPLUntypedBools.