proposition: Lemma foreach_union_eq : forall P E F, foreach P (E \u F) = (foreach P E /\ foreach P F).
proof: Proof. Proof using. intros. extens. iff. apply~ foreach_union_inv. apply* foreach_union. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)