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).

Lemma true_cannot_be_evaluated : forall t, ~ evaluate Ttrue t.
Proof.
  intro t. intro H. inversion H.
Qed.

Lemma false_cannot_be_evaluated : forall t, ~ evaluate Tfalse t.
Proof.
  intro t. intro H. inversion H.
Qed.

Theorem th_3_5_5 : forall t t' t'', evaluate t t' -> evaluate t t'' -> t' = t''.
Proof.
  induction 1.
  intro H. inversion H. reflexivity. contradict H4. apply true_cannot_be_evaluated.
  intro H. inversion H. reflexivity. contradict H4. apply false_cannot_be_evaluated.
  admit.
Qed.