Add `big_sepM2_union_inv_*`.

I needed a lemma like this a couple of times. The proof ends up being quite long.

I can also add a symmetric case big_sepM2_union_inv_r, but I am not sure if there is a better way of proving it than copy-pasting the proof for the _l case.