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
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