\begin{equation}
|(M.forall a, x) ordered x ==> ordered (insert a x)|,
\end{equation}
\begin{equation}
|(M.forall M.x, M.y) ordered M.x /\ ordered M.y ==> ordered (merge M.x M.y)|.
\end{equation}