proposition: Lemma typing_unique : forall E Pt T (d1 d2 : Typing E Pt T), d1 = d2.
proof: Proof. refine( fix Deriv_unique e t T (d1 d2 : Typing e t T) {struct d1} : d1 = d2 := match d1 as d1' in Typing e1 t1 T1, d2 as d2' in Typing e2 t2 T2 return forall (cast : (e1,t1,T1) = (e2,t2,T2)), (e1,t1,T1) = (e,t,T) -> eq_rect (e1,t1,T1) (fun etT => match etT with (e,t,T) => Typing e t T end) d1' _ cast = d2' with | TVar _, TVar _ => _ | TFun _ _, TFun _ _ => _ | TAbs _, TAbs _ => _ | TApp _ _, TApp _ _ => _ | _, _ => _ end (eq_refl _) (eq_refl _)); intros; destruct t; try discr; try discr cast; try discr dis; injection cast; intros; gen cast; clear cast. revert v v0. rewrite H0; rewrite H1; rewrite H2. intros; pattern cast; apply (K_dec_type eq_EPS_dec). rewrite (VarD_unique v v0); apply eq_refl. rewrite H1; rewrite H2. intros; pattern cast; apply (K_dec_type eq_EPS_dec); apply eq_refl. revert t1. rewrite <- H0; rewrite <- H1; rewrite <- H2; rewrite <- H4. intros; pattern cast; apply (K_dec_type eq_EPS_dec). rewrite(Deriv_unique _ _ _ t0 t1); apply eq_refl. revert t2 t3. rewrite <- H0; rewrite <- H1; rewrite <- H2; rewrite <- H3. intros t2 t3. intros; pattern cast; apply (K_dec_type eq_EPS_dec). set(h1 := Type_unique t0 t2); injection h1; intro H7. clear h1. revert t2 t3. rewrite <- H7. intros; rewrite(Deriv_unique _ _ _ t0 t2); rewrite(Deriv_unique _ _ _ t1 t3); apply eq_refl. Qed.
imports: Coq(Eqdep_dec) CoLoR(RelExtras ListExtras LogicUtil)