bool.v

Inductive term : Type :=
  | Ttrue : term
  | Tfalse : term
  | Tifthenelse : term -> term -> term -> term.

Inductive evaluate : term -> term -> Prop :=
  | Eiftrue : forall t2 t3, evaluate (Tifthenelse Ttrue t2 t3) t2
  | Eiffalse : forall t2 t3, evaluate (Tifthenelse Tfalse t2 t3) t3
  | Eif : forall t1 t1' t2 t3, evaluate t1 t1' -> evaluate (Tifthenelse t1 t2 t3) (Tifthenelse t1' t2 t3).

Theorem th_3_5_5 : forall t t' t'', evaluate t t' -> evaluate t t'' -> t' = t''.
Proof.
  admit.
Qed.