proposition: Lemma foreach_single_eq : forall P X, foreach P (\{X}:multiset A) = P X.
proof: Proof. Proof using. intros. extens. iff. apply H. apply in_single_self. apply~ foreach_single. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)