proposition: Lemma mem_spec : forall (s : t) (x : elt) (Hs : Ok s), mem x s = true <-> In x s.
proof: Proof. induction s; intros x Hs; inv; simpl. - intuition. + discriminate. + inv. - elim_compare x a; rewrite InA_cons; intuition; try order. + discriminate. + sort_inf_in. order. + rewrite <- IHs; auto. + rewrite IHs; auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists