proposition: Lemma foreach_remove : forall P E F, (forall x, x \in E -> x \notin F -> P x) -> foreach P (E \- F).
proof: Proof. Proof using. introv M Px. rewrite in_remove_eq in Px. applys* M. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)