This MR adds a more general version of
big_sepM_impl. The current
big_sepM_impl requires the map in the assumption and conclusion to be exactly the same. The variant in this MR allows the maps to be different. They don't have to agree in their overlap and the domain of the map in the assumption can be both smaller or larger than the domain of the map in the conclusion.
big_sepM_impl_strong is the fully general lemma and
big_sepM_impl_dom_subseteq is a variant that is easier to use when one knows that the map in the assumption is defined for at least as many keys as the map in the conclusion.
Note: Both the lemmas require
Ψ to be affine since the map in the assumption may be larger and stuff from it may be thrown away. One can imagine variants of these lemmas where the initial map is only allowed to be smaller and where the affine requirement is lifted. For my use case I needed this more general variant though.
Note: This generalization makes sense for some of the other
big_sep*_impl as well but I only needed it for
big_sepM. If adding it for some of the others is not too much additional work then I can do that as well, but I would prefer not to