Skip to content

Add `big_opM_union` and `big_sepM_union`.

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

I couldn't find an easier way to prove big_sepM_union.

Merge request reports