I'll check this other paper. I've started reading the PhD manuscript of Carsten, around page 100 I found this (SOME...BLOCK...) syntax. It indeed seems that in our proofs/criteria it may make sense to reason about a context block as a whole. Thanks again for the pointers.