proposition: Lemma for_all_spec: forall s f, @compat_bool elt E.eq f -> (for_all f s = true <-> For_all (fun x => f x = true) s).
proof: Proof. intros. apply xforall_spec. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface