proposition: Lemma foreach_union_inv : forall P E F, foreach P (E \u F) -> foreach P E /\ foreach P F.
proof: Proof. Proof using. introv H. split; introv K. apply H. rewrite~ @in_union_eq. typeclass. apply H. rewrite~ @in_union_eq. typeclass. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)