# Add generalized implication lemma for big_sepM

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.

The lemma `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 ~~`Φ`

and `Ψ`

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