Merge branch 'robbert/map_disjoint_difference' into 'master'

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

See merge request !551