proposition: Lemma remove_fv_rename x y u : ~In y (fv u) -> remove y (fv (rename x y u)) [=] remove x (fv u).
proof: Proof. intro hy. rewrite fv_rename; unfold replace. case_eq (mem x (fv u)); intro hx. apply remove_add. set_iff. tauto. rewrite remove_equal. 2: hyp. rewrite remove_equal. refl. rewrite mem_iff, hx. discr. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)