proposition: Lemma tr_fv_dom : forall E v V, E |- v ~: V -> fv v [<=] dom E.
proof: Proof. induction 1; simpl; intro z; set_iff. intro e. subst z. rewrite In_dom. exists T. hyp. tauto. intros [h|h]. apply IHtr1. hyp. apply IHtr2. hyp. intros [h1 h2]. rewrite In_dom, <- add_neq_in_iff. 2: apply h2. rewrite <- In_dom. apply IHtr. hyp. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)