proposition: Lemma inter_Intersection : forall s s', !!(inter s s') === Intersection _ (!!s) (!!s').
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