proposition: Lemma var_notin_fvcod x u s : ~In (var x u s) (fvcod (remove x (fv u)) s).
proof: Proof. rewrite In_fvcod. intros [y [h1 h]]. revert h1. set_iff. intros [hy n]. eapply var_notin_fv_subs. apply hy. 2: apply h. auto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)