proposition: Lemma filter_spec : compatb f -> (In x (filter f s) <-> In x s /\ f x = true).
proof: Proof. exact (@M.filter_spec _ _ _). Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts