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