proposition: Lemma singleton_Singleton : forall x, !!(M.singleton x) === Singleton _ x .
proof: Proof. unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1; try constructor; auto. Qed.
imports: Ensembles Finite_sets MSetInterface MSetProperties OrdersEx