proposition: Lemma single_var x u s v z : In z (fv u) -> x <> z -> subs (single (var x u s) v) (s z) = s z.
proof: Proof. intros h1 h2. rewrite single_notin_fv. refl. unfold Def.var; ens. case_eq (mem x (fvcodom (remove x (fv u)) s)). rewrite <- mem_iff. set (xs := union (fv u) (fvcodom (remove x (fv u)) s)). gen (var_notin_ok xs). set (x' := var_notin xs). unfold xs. set_iff. intros h hx g. apply h. right. rewrite In_fvcodom. exists z. set_iff. destruct (eq_term_dec (s z) (Var z)). 2: tauto. revert g. rewrite e. simpl. set_iff. intro g. subst z. tauto. rewrite <- not_mem_iff. intros h3 h4. apply h3. rewrite In_fvcodom. exists z. set_iff. destruct (eq_term_dec (s z) (Var z)). 2: tauto. revert h4. rewrite e. simpl. set_iff. intro h4. subst z. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)