proposition: Lemma fv_rename y z u : fv (rename y z u) [=] replace y z (fv u).
proof: Proof. unfold Def.rename, replace. rewrite fv_single. simpl. destruct (mem y (fv u)). intro a. set_iff. tauto. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)