proposition: Lemma for_all_spec s f : Proper (X.eq==>eq) f -> (for_all f s = true <-> For_all (fun x => f x = true) s).
proof: Proof. intros Hf; unfold For_all. induction s as [|i l IHl x r IHr]; simpl; auto. - split; intros; inv; auto. - rewrite <- !andb_lazy_alt, !andb_true_iff, IHl, IHr. clear IHl IHr. intuition_in. eauto. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat