proposition: Lemma var_notin_fvcodom x u s : ~In (var x u s) (fvcodom (remove x (fv u)) s).
proof: Proof. unfold Def.var; ens. set (xs := fvcodom (remove x (fv u)) s). case_eq (mem x xs). gen (var_notin_ok (union (fv u) xs)). set_iff. tauto. rewrite <- not_mem_iff. auto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)