Zakky.v

Inductive Term : Set :=
 | T
 | F
 | TIf (_ : Term) (_ : Term) (_ : Term).

Inductive Step : Term -> Term -> Prop :=
 | EIfTrue  : forall (t1 t2 : Term), Step (TIf T t1 t2) t1
 | EIfFalse : forall (t1 t2 : Term), Step (TIf F t1 t2) t2
 | EIf      : forall (t1 t1' t2 t3 : Term), Step t1 t1' -> Step (TIf t1 t2 t3) (TIf t1' t2 t3).

Lemma dec: forall (t t' t'' : Term),
  Step t t' -> Step t t'' -> t' = t''.
Proof.
  Check Step_ind.
  intros t t' t'' Q.

  generalize t''.
  apply Step_ind with (t:=t) (t0:=t'); intros; auto.
    inversion H; auto.
    inversion H4.

    inversion H; auto.
    inversion H4.

    destruct t1.
      inversion H.
      inversion H.

      inversion H1.
      apply H0 in H6.
      rewrite H6.
      reflexivity.
Qed.