proposition: Lemma is_empty_spec : forall s : t, is_empty s = true <-> Empty s.
proof: Proof. intros [ | x s]; simpl. - split; auto. intros _ x H. inv. - split. + discriminate. + intros H. elim (H x); auto. Qed.
imports: MSetInterface OrdersFacts OrdersLists