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.