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 frameR
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 steptaking 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.