proposition: Lemma union_Union : forall s s', !!(union s s') === Union _ (!!s) (!!s').
proof: Proof. unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1; [ constructor 1 | constructor 2 | | ]; auto. Qed.
imports: Ensembles Finite_sets MSetInterface MSetProperties OrdersEx