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.
  intros t t' t'' H. revert t''. induction H; intros t'' H0; inversion H0; try reflexivity.
    contradict H4. apply true_cannot_be_evaluated.
    contradict H4. apply false_cannot_be_evaluated.
    rewrite <- H2 in H. contradict H. apply true_cannot_be_evaluated.
    rewrite <- H2 in H. contradict H. apply false_cannot_be_evaluated.
    f_equal. apply IHevaluate. apply H5.
Qed.