proposition: Lemma notin_of_foreach_not : forall P x E, foreach P E -> ~ P x -> x \notin E.
proof: Proof. Proof using. introv M N I. applys N. applys~ M. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)