Remove basic updates from the Iris model, and define them using plainly.

In this MR, I define basic updates as:

|==> P  :=  (∀ R, (P -∗ ■ R) -∗ ■ R)

This is the continuation monad, where one should think of ■ R being the final result that one wants to get out of the soundness theorem. The proposition R needs to be plain (i.e. wrapped in ■) because we can only get resource independent propositions out of the soundness theorem.

From this definitions, we can prove all laws of basic updates, apart from those related to frame preserving updates. For that, we need the following primitive rule:

x ~~>: Φ →
uPred_ownM x ∗ (∀ y, ⌜Φ y⌝ -∗ uPred_ownM y -∗ ■ R) ⊢ ■ R.

This rule could be read as: If we want to prove the final result while owning x, we could also prove it while owning any y to which we could do a frame preserving update.

---

So, in total, this gets rid of 1 primitive connective (|==>) and 5 primitive rules (those of |==>), which is replaced by one new primitive rule.

This MR is an alternative to !172 (closed), and is a much simplified version of @amintimany's proposal in that MR.