Skip to content

Add `big_sepM2_union_inv_*`.

Dan Frumin requested to merge dfrumin/iris-coq:big_sepM2_lemmata into master

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.

Edited by Dan Frumin

Merge request reports