proposition: Lemma domain_union s p q : domain (union p q) s [=] union (domain p s) (domain q s).
proof: Proof. intro x. set_iff. rewrite !In_domain. set_iff. tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)