Skip to content
GitLab

big_sepM2 and associated lemmas

Merged Dan Frumin requested to merge dfrumin/iris-coq:robbert/big_sepM2 into master

Following big_sepL2 and big_sepM. Based on some code from @robbertkrebbers.

Would like to hear your comments and also add some helpful lemmas about this big op.

Edited by Dan Frumin