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