proposition: Lemma Equal_Same_set : forall s s', s[=]s' <-> !!s === !!s'.
proof: Proof. intros. rewrite double_inclusion. unfold Subset, Included, Same_set, In, mkEns; intuition. Qed.
imports: Ensembles Finite_sets MSetInterface MSetProperties OrdersEx