Strengthen `map_disjoint_difference_{l,r}` and make them consistent with the lemmas for sets.

This closes #208 (closed), if m2 = m3 the precondition is vacuously true.