Repair the plainly modality

Change proposition extensionality into:

bi_plainly ((P -∗ Q) ∧ (Q -∗ P)) ⊢ P ≡ Q

This was suggested by @jjourdan, and @amintimany proved that this axiom holds in the ordered RA model. This MR shows that it also holds for monPred. This should thus solve the paradox in #149 (closed).

If we accept this MR, I don't think there is a need for !98 (closed) anymore. It shows that we can define a plainly modality on any logic we currently care about.

At the same time, this MR removes the following axiom for plainly:

bi_plainly (bi_persistently P) ⊢ bi_plainly P

This axiom turned out to be admissible.

In terms of axioms, I very much like the current axioms. This way, plainly behaves in the same way as persistently and bi_valid.