Skip to content

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

Robbert Krebbers requested to merge robbert/map_disjoint_difference into master

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

Merge request reports