proposition: Lemma for_all_2 : 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 s f _. unfold for_all. rewrite xforall_spec. trivial. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface