Skip to content

Added a stronger version of cinv_open_strong

Jonas Kastberg requested to merge jihgfee/iris-coq:cinv_open_stronger into master

cinv_open_strong is not as strong as inv_open_strong, namely since you cannot pick the closing mask at a later time. This commit addes a new lemma cinv_open_stronger which does just that.

Simply replacing the lemma broke some proofs, but I can bump them if that is deemed better.

Merge request reports