proposition: Lemma fvcodom_rename y z xs : fvcodom xs (single y (Var z)) [=] if mem y xs && negb (eqb z y) then singleton z else empty.
proof: Proof. rewrite fvcodom_single, beq_term_var. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)