proposition: Lemma fvcod_rename y z xs : fvcod xs (single y (Var z)) [=] if mem y xs then add z (remove y xs) else xs.
proof: Proof. rewrite fvcod_single. simpl. destruct (mem y xs). intro a. set_iff. tauto. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)