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.