proposition: Lemma fvcod_subset_fv_subs s u : fvcod (fv u) s [<=] fv (subs s u).
proof: Proof. rewrite fv_subs. simpl. intro x. rewrite In_fvcod. intros [y [h1 h2]]. set_iff. rewrite In_domain. fold (fvcodom (fv u) s). rewrite In_fvcodom. destruct (eq_term_dec (s y) (Var y)). left. revert h2. rewrite e. simpl. set_iff. intro h2. subst y. tauto. right. exists y. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)