proposition: Lemma Add_Add : forall x s s', MP.Add x s s' -> !!s' === Add _ (!!s) x.
proof: Proof. unfold Same_set, Included, mkEns, In. split; intros. - red in H; rewrite H in H0. destruct H0. + inversion H0. constructor 2; constructor. + constructor 1; auto. - red in H; rewrite H. inversion H0; auto. inversion H1; auto. Qed.
imports: Ensembles Finite_sets MSetInterface MSetProperties OrdersEx