More principled set of axioms for fancy updates and plainly

This MR proposes a new set of axioms for the BiFUpdPlainly interface, namely:

fupd_plainly_mask_empty E (P : PROP) :
  (|={E,∅}=> ■ P) ⊢ |={E}=> P;
fupd_plainly_frame_r E (P R : PROP) :
  (R ={E}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R;
fupd_plainly_later E (P : PROP) :
  (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P;
fupd_plainly_forall_2 E {A} (Φ : A → PROP) :
  (∀ x, |={E}=> ■ Φ x) ⊢ |={E}=> ∀ x, Φ x

Contrary to what we had before, I think these axioms are more principled: all of these axioms do exactly one thing, which I believe can be explained.

• fupd_plainly_mask_empty : When proving a fancy update of a plain proposition, you can also prove it while being allowed to open all invariants.
• fupd_plainly_frame_r : A stronger version of the usual framing rule. The difference is that you get the frame R back for proving the remaining proposition, which should be plain to make that possible.
• fupd_plainly_later : Laters commute with fancy updates over plain propositions.
• fupd_plainly_forall_2 : Forall quantifiers commute with fancy updates over plain propositions.

This merge request closes #164 (closed).

Note that the result in !183 (closed) follows from the new laws. We can show that universal quantifiers commute with step-taking fancy updates, using just the above laws.

As part of this MR I also ported the adequacy proof of total weakest preconditions to the new style.

I directly took the liberty to clean up some of the derived results about the interaction between fancy updates and the plain modality.