proposition: Lemma fv_single y v u : fv (subs (single y v) u) [=] if mem y (fv u) then union (remove y (fv u)) (fv v) else fv u.
proof: Proof. rewrite fv_subs. simpl. rewrite domain_single, fvcod_single. case_eq (mem y (fv u)); intro hy; simpl. unfold bool_of_rel. case (eq_term_dec v (Var y)); intro hv; simpl. subst. simpl. rewrite <- mem_iff in hy. rewrite empty_b. intro a. set_iff. split. intros [[a1 _]|a1]. eq_dec y a; subst; auto. contr. intros [[a1 a2]|a1]; subst; auto. rewrite singleton_b, eqb_refl. intro a. set_iff. tauto. rewrite empty_b. intro a. set_iff. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)