proposition: Lemma for_all_spec : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> (for_all f s = true <-> For_all (fun x => f x = true) s).
proof: Proof. unfold For_all; induction s; simpl. - intuition. inv. - intros; inv. destruct (f a) eqn:F. + rewrite IHs; intuition. inv; auto. setoid_replace x with a; auto. + split; intros H'; try discriminate. intros. rewrite <- F, <- (H' a); auto. Qed.
imports: MSetInterface