proposition: Lemma exists_spec : compatb f -> (exists_ f s = true <-> Exists (fun x => f x = true) s).
proof: Proof. exact (@M.exists_spec _ _). Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts