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.