Added a stronger version of cinv_open_strong
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.