proposition: Lemma tr_restrict : forall E v V, E |- v ~: V -> restrict_dom E (fv v) |- v ~: V.
proof: Proof. induction 1; simpl. apply tr_var. apply mapsto_restrict_dom_singleton. hyp. apply tr_fun. apply tr_app with V; eapply tr_le. eapply restrict_dom_s. refl. apply union_subset_1. refl. refl. hyp. eapply restrict_dom_s. refl. apply union_subset_2. refl. refl. hyp. apply tr_lam. eapply tr_le. 2: refl. 2: refl. 2: apply IHtr. intros y hy. env. rewrite mapsto_restrict_dom, !add_mapsto_iff, mapsto_restrict_dom. set_iff. tauto. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)