proposition: Lemma typing_c_unique : forall E e T1 T2, typing_c E e T1 -> typing_c E e T2 -> T1 = T2.
proof: Proof. intros E e T1 T2 Typ1 Typ2. generalize dependent T2. induction Typ1; intros T' Typ'; inversion Typ'; subst; eauto. Case "typing_var_c". eapply binds_unique; eauto. Case "typing_abs_c". f_equal; eauto. pick fresh x. apply (H0 x); eauto. Case "typing_app_c". assert (typ_arrow T1 T2 = typ_arrow T0 T') by auto. inversion H; eauto. Qed.
imports: Metalib.Metatheory String