proposition: Lemma Type_unique : forall Pt E T1 T2 (d1 : Typing E Pt T1) (d2 : Typing E Pt T2), T1 = T2.
proof: Proof. induction Pt; intros; inversion d1; inversion d2; trivial. unfold VarD in * . assert(Some (Some T1) = Some (Some T2)). trans (nth_error E x); auto. injection H7; trivial. rewrite(@IHPt _ _ _ X X0); auto. set(e0 := IHPt1 _ _ _ X X1); injection e0; auto. Qed.
imports: Coq(Eqdep_dec) CoLoR(RelExtras ListExtras LogicUtil)