Show that for non-step indexed BIs, <pers> can trivially be inhabited.
See my comment in !843 (closed):
I just realized that there might be a different approach to support BIs without persistence modality. You can define <pers> P := ⌜ emp ⊢ P ⌝
and prove all the laws if:
- The BI is discrete, that is
P ≡{n}≡ Q → P ≡ Q
- The BI enjoys the existential property:
emp ⊢ ∃ x, Φ x
implies∃ x, emp ⊢ Φ x
In fact, I even realized I have done this in my course, where I let my students build a classical separation logic, and use that to instantiate the proof mode in my subsequent lectures.