Skip to content

Add `big_sepL2_app_inv_2`.

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

This is a useful lemma (at least for me), and I don't think it's directly derivable from the other two _inv lemmas.

Merge request reports