proposition: Lemma for_all_1 : forall (s : t) (f : elt -> bool), compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true.
proof: Proof. intros s f; unfold for_all; case M.for_all; intuition; elim n; auto. Qed.
imports: FSetInterface