Inductive term : Set :=
  | True : term
  | False : term
  | If : term -> term -> term -> term.

Inductive evalR : term -> term -> Prop := 
  | EIfTrue  : forall (t2 t3 : term), evalR (If True t2 t3) t2
  | EIfFalse : forall (t2 t3 : term), evalR (If False t2 t3) t3
  | EIf      : forall (t1 t1' t2 t3 : term), evalR t1 t1' -> evalR (If t1 t2 t3) (If t1' t2 t3).

Theorem eval_determinacy :
  forall t t' t'' : term, evalR t t' -> evalR t t'' -> t' = t''.
Proof.
intros t t' t'' t'deriv.
elim t'deriv.
intros t2 t3 t4.
inversion t4.
trivial.
inversion H3.
intros t2 t3 t4.
inversion t4.
trivial.
inversion H3.
intros t1 t1' t2 t3.
intros.