Rename a couple of theorems about multiset ordering.

There are two characterisations of the transitive closure of the
one-step process (which takes one element out and replaces it with a
multiset of elements, all of which are R-smaller than the removed
element).

In each, a multiset is removed, and a dominated multiset is put back.
If, as is typical, R is well-founded and transitive, the removed
multiset can be made disjoint with the added multiset.  But when
attempting to prove that two multisets are related this way, there's
no need to require that they be disjoint.  Contrariwise, the
disjointness condition might be useful if one has the ordering as an
assumption.

This change makes sure that both characterisations are exported, with
the names mlt_dominates_thm1 and mlt_dominates_thm2.  Previously only
mlt_dominates_thm2 was saved, and that with the name
mlt_dominates_thm.