proposition: Lemma fvcodom_union s p q : fvcodom (union p q) s [=] union (fvcodom p s) (fvcodom q s).
proof: Proof. intro x. set_iff. unfold Def.fvcodom. rewrite domain_union, fvcod_union. set_iff. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)