Coq: trying to use dependent induction

The issue is that, by default, Coq does not generate dependent induction principles for propositions. We can fix this by overriding this default:

Require Import Coq.Program.Equality.

Inductive type : Set :=
| TInt
| TFun: type -> type -> type
| TStar
.

Reserved Infix "<|" (at level 80).

(* Ensure Coq does not generate TPrecision_ind when processing this definition *)
Unset Elimination Schemes.
Inductive TPrecision : type -> type -> Prop :=   (* see below *)
| PRInt : TInt <| TInt
| PRFun : forall t1 t2 t1' t2',
    t1 <| t2 -> t1' <| t2' -> TFun t1 t1' <| TFun t2 t2'
| PRStar : forall t, t <| TStar

  where "x '<|' y" := (TPrecision x y).
(* Re-enable automatic generation *)
Set Elimination Schemes.

(* Compare the following induction principle with the one generated by Coq by
default. *)
Scheme TPrecision_ind := Induction for TPrecision Sort Prop.

Lemma TP_unique: forall t1 t2 (P1 P2 : t1 <| t2), P1 = P2.
Proof.
  intros.
  dependent induction P1; dependent destruction P2; trivial.
  f_equal; auto.
Qed.