proposition: Lemma Empty_Empty_set : forall s, Empty s -> !!s === Empty_set _.
proof: Proof. unfold Same_set, Included, mkEns, In. split; intros. - destruct(H x H0). - inversion H0. Qed.
imports: Ensembles Finite_sets MSetInterface MSetProperties OrdersEx