proposition: Lemma tr_contraction : forall E v V, E |- v ~: V -> forall y, ~XSet.In y (fv v) -> remove y E |- v ~: V.
proof: Proof. induction 1 ; intro y; simpl; set_iff; intro hy. apply tr_var. apply remove_2; auto. apply tr_fun. apply tr_app with V. apply IHtr1. tauto. apply IHtr2. tauto. apply tr_lam. try rename X into X0. eq_dec x y. eapply tr_le with (x:=add x X0 E). 2: refl. 2: refl. intros z hz. env. do 2 rewrite find_mapsto_iff, add_o. eq_dec x z; auto. rewrite remove_o. eq_dec y z. exfalso. apply n. trans y; hyp. auto. hyp. eapply tr_le with (x:= remove y (add x X0 E)). 2: refl. 2: refl. intros z hz. env. rewrite !find_mapsto_iff, add_o, !remove_o, add_o. eq_dec y z. discr. eq_dec x z; auto. apply IHtr. tauto. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)