move persistently_forall_2 out of BI interface
This is a step towards #224: weaken the BI axioms such that IPM can support logics where the persistently modality is defined with an existential quantifier. This means we have to remove persistently_forall_2
and replace it by the weaker persistently_and_2
(so only finite conjunction can be commuted around <pers>
). We also have to remove persistently_impl_plainly : (■ P → <pers> Q) ⊢ <pers> (■ P → Q)
from BiPlainly
-- I don't think this can be proven constructively for ∃-based <pers>
, though there might be a classical proof.
I then added typeclasses so that logics that do enjoy the full set of properties can still exploit them. For users of uPred
and its derivatives, there should be no changes.
Edited by Ralf Jung