Vladimir_Nesov comments on Probabilistic Payor Lemma?

[Vladimir_Nesov]

The lemma was proved using the same modal assumptions as Löb’s

I think the lemma doesn’t need internal necessitation ($⊢\square A\to \square \square A$). Though it’s still referenced in a proof of non-exploitability.