proposition: Lemma fvcodom_single y v xs : fvcodom xs (single y v) [=] if mem y xs && negb (beq_term v (Var y)) then fv v else empty.
proof: Proof. unfold Def.fvcodom. rewrite domain_single, fvcod_single. unfold bool_of_rel. case_eq (mem y xs); intro hy; destruct (eq_term_dec v (Var y)); simpl; try rewrite empty_b. refl. rewrite singleton_b, eqb_refl, singleton_equal_add, remove_add, empty_union_2. refl. apply empty_1. set_iff. tauto. refl. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)