proposition: Lemma foreach_union : forall P E F, foreach P E -> foreach P F -> foreach P (E \u F).
proof: Proof. Proof using. intros_all. destruct~ (in_union_inv H1). Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)