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.

mentioned in commit 3c8baa66

merged

mentioned in issue #208 (closed)