proposition: Lemma fv_replace_all x y : forall u, ~In y (bv u) -> ~In y (fv u) -> fv (replace_all x y u) [=] if mem x (fv u) then add y (remove x (fv u)) else fv u.
proof: Proof. induction u; simpl; set_iff; intros h1 h2; mem. unfold Def.replace_var. eq_dec x0 x. subst. fset. refl. refl. rewrite IHu1; [idtac|fo|fo]. rewrite IHu2; [idtac|fo|fo]. case_eq (mem x (fv u1)); case_eq (mem x (fv u2)); simpl; try (rewrite <- mem_iff); try (rewrite <- not_mem_iff); intros i1 i2. rewrite remove_union, !add_union_singleton, union_assoc, <- union_assoc with (s:=remove x (fv u1)), union_sym with (s:=remove x (fv u1)), union_assoc, union_idem_1. refl. rewrite remove_union, remove_equal with (s:=fv u2), union_add; fo. rewrite remove_union, remove_equal with (s:=fv u1), union_sym, union_add, union_sym; fo. refl. rewrite IHu; [idtac|fo|fo]. unfold Def.replace_var. eq_dec x0 x; simpl; bool. subst. case_eq (mem x (fv u)); try (rewrite <- mem_iff); try (rewrite <- not_mem_iff); intro h. rewrite remove_add. refl. set_iff. fo. rewrite !remove_equal. refl. fo. fo. case_eq (mem x (fv u)); try (rewrite <- mem_iff); try (rewrite <- not_mem_iff); intro h. rewrite <- remove_add_com, remove_com; fo. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)