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