proposition: Lemma var_notin_fv_subs x u s y : In y (fv u) -> y <> x -> ~In (var x u s) (fv (s y)).
proof: Proof. intros hy n h. apply var_notin_fvcodom with (x:=x) (u:=u) (s:=s). rewrite In_fvcodom. exists y. set_iff. intuition. revert h. rewrite H. simpl. set_iff. intro e. set (xs := fvcodom (remove x (fv u)) s). revert e; unfold Def.var; ens; intro e. fold xs in e. case_eq (mem x xs); intro i; rewrite i in e. 2: fo. gen (var_notin_ok (union (fv u) xs)); intro h. apply h. rewrite <- e, <- union_subset_1. hyp. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)