Draft: move bi_persistently_emp out of BI interface, and get a basic proof mode working again
This makes the proofmode work with an arbitrary BI, even ones that do not have a sensible persistence modality: one can pick const False
as the modality to satisfy all the remaining mandatory laws.
Based on !881 (merged) Fixes #425