proposition: Lemma fv_subs : forall u s, fv (subs s u) [=] let xs := domain (fv u) s in union (diff (fv u) xs) (fvcod xs s).
proof: Proof. induction u; simpl; intro s. rewrite singleton_equal_add, domain_add, domain_empty. 2: firstorder auto with set. unfold Def.domain_fun, bool_of_rel. destruct (eq_term_dec (s x) (Var x)). rewrite e. simpl. rewrite fvcod_empty. fset. rewrite fvcod_add, fvcod_empty. 2: set_iff; fo. unfold Def.fvcod_fun. intro a. set_iff. split. intro h. auto. intros [[h1 h2]|[h1|h1]]; fo. intro y. rewrite domain_empty, fvcod_empty. set_iff. tauto. rewrite IHu1, IHu2. simpl. intro y. set_iff. rewrite !In_fvcod, !In_domain. set_iff. split_all; try tauto. right. ex x. revert H. rewrite !In_domain. set_iff. tauto. right. ex x. revert H. rewrite !In_domain. set_iff. tauto. revert H. rewrite In_domain. set_iff. split_all. left. right. ex x. rewrite In_domain. tauto. right. right. ex x. rewrite In_domain. tauto. unfold Def.var, Def.fvcodom; ens. set (xs := fvcod (domain (remove x (fv u)) s) s). case_eq (mem x xs); [rewrite <- mem_iff|rewrite <- not_mem_iff]; intro hx; simpl; rewrite IHu; simpl. set (x' := var_notin (union (fv u) xs)). gen hx. unfold xs at 1. rewrite In_fvcod. intros [z hz]. revert hz. rewrite In_domain. set_iff. split_all. intro y. set_iff. rewrite !In_domain, In_fvcod. unfold Def.update at 1. eq_dec y x. subst y. set_iff. split_all. right. exists z. rewrite In_domain. unfold Def.update. eq_dec z x. subst z. tauto. tauto. subst x'. apply var_notin_ok with (xs := union (fv u) xs). rewrite H4. apply union_subset_2. hyp. set_iff. split_all. left. split_all. revert H3 H5. rewrite In_domain. unfold Def.update. eq_dec x0 x; simpl; set_iff. subst x0. intuition. destruct (In_dec y xs). auto. left. absurd (In y xs). hyp. unfold xs. rewrite In_fvcod. exists x0. rewrite In_domain. set_iff. fo. tauto. revert H3. unfold xs. rewrite In_fvcod. intros [a ha]. revert ha. rewrite In_domain. set_iff. split_all. right. exists a. rewrite In_domain. unfold Def.update. eq_dec a x. subst a. cong. tauto. subst y. absurd (In x' (union (fv u) xs)). apply var_notin_ok. apply union_subset_1. hyp. subst y. absurd (In x' (union (fv u) xs)). apply var_notin_ok. apply union_subset_2. hyp. intro y. set_iff. rewrite !In_domain. set_iff. rewrite In_fvcod. unfold Def.update. eq_dec y x. subst y. tauto. split_all; try tauto. revert H. rewrite In_domain. eq_dec x0 x. subst x0. tauto. split_all. right. unfold xs. rewrite In_fvcod. exists x0. rewrite In_domain. set_iff. fo. revert H. unfold xs. rewrite In_fvcod. intros [z hz]. revert hz. rewrite In_domain. set_iff. split_all. right. exists z. rewrite In_domain. eq_dec z x. subst z. tauto. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)