diff --git a/CHANGELOG.md b/CHANGELOG.md
index b7958f09c1d0fe3824761ca8ec2b15746e97f0a5..caee82ff7153e4c274b907bd51be0535d90cd195 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -205,6 +205,12 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Move the RAs for `nat` and `positive` and the `mnat` RA into a separate
   module. They must now be imported from `From iris.algebra Require Import
   numbers`.
+* Remove notation for 3-mask step-taking updates, and made 2-mask notation less
+  confusing by distinguishing it better from mask-changing updates.
+  Old: `|={E1,E2}â–·=> P`. New: `|={Eo}[Ei]â–·=> P`.
+  As part of this, the lemmas about the 3-mask variant were changed to be about
+  the 2-mask variant instead, and `step_fupd_mask_mono` now also has a more
+  consistent argument order for its masks.
 
 The following `sed` script should perform most of the renaming (FIXME: incomplete)
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index ce392cb8229ae41519d8e9a9d7f8a7b5367bd119..6cdf3d284cc2c909e4bbaa9110099bc4849cca24 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -70,7 +70,7 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
-  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤,∅}▷=>^n |={⊤,∅}=> ⌜ φ ⌝) →
+  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n |={⊤,∅}=> ⌜ φ ⌝) →
   φ.
 Proof.
   intros Hiter.
@@ -88,7 +88,7 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
-  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤,∅}▷=>^n ⌜ φ ⌝)  →
+  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   iIntros (Hiter). eapply (step_fupdN_soundness _ n).
diff --git a/theories/bi/ascii.v b/theories/bi/ascii.v
index 1a9eec4630ab747f306cb37bf668678d02c0b523..0f955957782cf7e69bed088d0dead44669de592f 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -85,28 +85,21 @@ Notation "P ={ E }=* Q" := (P ={E}=∗ Q)
   (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope
 .
 
-Notation "|={ E1 , E2 , E3 }|>=> Q" := (|={E1,E2,E3}â–·=> Q)%I
-  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "P ={ E1 , E2 , E3 }|>=* Q" := (P ={E1,E2,E3}▷=∗ Q)%I
-  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "|={ E1 , E2 }|>=> Q" := (|={E1,E2}â–·=> Q)%I
-  (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
-
-Notation "P ={ E1 , E2 }|>=* Q" := (P ={E1,E2}▷=∗ Q)
+Notation "P ={ E1 } [ E2 ]|>=* Q" := (P ={E1}[E2]▷=∗ Q)
   (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ={ E1 , E2 }|>=* Q" := (P ={E1,E2}▷=∗ Q)%I
+Notation "P ={ E1 } [ E2 ]|>=* Q" := (P ={E1}[E2]▷=∗ Q)%I
   (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
 
 Notation "|={ E }|>=> Q" := (|={E}â–·=> Q)%I
   (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
 Notation "P ={ E }|>=* Q" := (P ={E}▷=∗ Q)%I
   (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "|={ E1 , E2 }|>=>^ n Q" := (|={E1,E2}â–·=>^n Q)%I
+Notation "|={ E1 } [ E2 ]|>=>^ n Q" := (|={E1}[E2]â–·=>^n Q)%I
   (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
   : bi_scope.
-Notation "P ={ E1 , E2 }|>=*^ n Q" := (P ={E1,E2}▷=∗^n Q)%I
+Notation "P ={ E1 } [ E2 ]|>=*^ n Q" := (P ={E1}[E2]▷=∗^n Q)%I
   (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
    : stdpp_scope.
-Notation "P ={ E1 , E2 }|>=*^ n Q" := (P ={E1,E2}▷=∗^n Q)%I
+Notation "P ={ E1 } [ E2 ]|>=*^ n Q" := (P ={E1}[E2]▷=∗^n Q)%I
   (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
   : bi_scope.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index e6f02661858f300a1edc2b255cc0d8dcf716d985..99599c3beb55ddbd5b91094c9b3349dbd87ff632 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -93,30 +93,33 @@ Reserved Notation "P ={ E }=∗ Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[' P  '/' ={ E }=∗  Q ']'").
 
-Reserved Notation "|={ E1 , E2 , E3 }â–·=> Q"
+(** Step-taking fancy updates *)
+Reserved Notation "|={ E1 } [ E2 ]â–·=> Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 , E3 }â–·=>  Q").
-Reserved Notation "P ={ E1 , E2 , E3 }▷=∗ Q"
+   format "|={ E1 } [ E2 ]â–·=>  Q").
+Reserved Notation "P ={ E1 } [ E2 ]▷=∗ Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
-   format "'[' P  '/' ={ E1 , E2 , E3 }▷=∗  Q ']'").
-Reserved Notation "|={ E1 , E2 }â–·=> Q"
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }â–·=>  Q").
-Reserved Notation "P ={ E1 , E2 }▷=∗ Q"
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "'[' P  '/' ={ E1 , E2 }▷=∗  Q ']'").
+   format "'[' P  '/' ={ E1 } [ E2 ]▷=∗  Q ']'").
 Reserved Notation "|={ E }â–·=> Q"
   (at level 99, E at level 50, Q at level 200,
    format "|={ E }â–·=>  Q").
 Reserved Notation "P ={ E }▷=∗ Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[' P  '/' ={ E }▷=∗  Q ']'").
-Reserved Notation "|={ E1 , E2 }â–·=>^ n Q"
+
+(** Multi-step-taking fancy updates *)
+Reserved Notation "|={ E1 } [ E2 ]â–·=>^ n Q"
   (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
-   format "|={ E1 , E2 }â–·=>^ n  Q").
-Reserved Notation "P ={ E1 , E2 }▷=∗^ n Q"
+   format "|={ E1 } [ E2 ]â–·=>^ n  Q").
+Reserved Notation "P ={ E1 } [ E2 ]▷=∗^ n Q"
   (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
-   format "P  ={ E1 , E2 }▷=∗^ n  Q").
+   format "P  ={ E1 } [ E2 ]▷=∗^ n  Q").
+Reserved Notation "|={ E }â–·=>^ n Q"
+  (at level 99, E at level 50, n at level 9, Q at level 200,
+   format "|={ E }â–·=>^ n  Q").
+Reserved Notation "P ={ E }▷=∗^ n Q"
+  (at level 99, E at level 50, n at level 9, Q at level 200,
+   format "P  ={ E }▷=∗^ n  Q").
 
 (** * Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index ad8d6bbb0459dedf5fb71bdbfbeb85e4a4367e88..9690d30af7ac1eadb9089a1d3a45c3fbdad672b7 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -26,17 +26,32 @@ Notation "|={ E }=> Q" := (fupd E E Q) : bi_scope.
 Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I : bi_scope.
 Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q) : stdpp_scope.
 
-(** Fancy updates that take a step. *)
-Notation "|={ E1 , E2 , E3 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E3}=> Q))%I : bi_scope.
-Notation "P ={ E1 , E2 , E3 }▷=∗ Q" := (P -∗ |={ E1,E2,E3 }▷=> Q)%I : bi_scope.
-Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2,E1}â–·=> Q)%I : bi_scope.
-Notation "P ={ E1 , E2 }▷=∗ Q" := (P ⊢ |={ E1 , E2, E1 }▷=> Q) (only parsing) : stdpp_scope.
-Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q)%I : bi_scope.
-Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I : bi_scope.
-Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I : bi_scope.
-Notation "|={ E1 , E2 }▷=>^ n Q" := (Nat.iter n (λ P, |={E1,E2}▷=> P) Q)%I : bi_scope.
-Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P ⊢ |={E1,E2}▷=>^n Q)%I (only parsing) : stdpp_scope.
-Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P -∗ |={E1,E2}▷=>^n Q)%I : bi_scope.
+(** * Step-taking fancy updates. *)
+(** These have two masks, but they are different than the two masks of a
+    mask-changing update: in [|={Eo}[Ei]â–·=> Q], the first mask [Eo] ("outer
+    mask") holds at the beginning and the end; the second mask [Ei] ("inner
+    mask") holds around each â–·. This is also why we use a different notation
+    than for the two masks of a mask-changing updates. *)
+Notation "|={ Eo } [ Ei ]â–·=> Q" := (|={Eo,Ei}=> â–· |={Ei,Eo}=> Q)%I : bi_scope.
+Notation "P ={ Eo } [ Ei ]▷=∗ Q" := (P -∗ |={Eo}[Ei]▷=> Q)%I : bi_scope.
+Notation "P ={ Eo } [ Ei ]▷=∗ Q" := (P -∗ |={Eo}[Ei]▷=> Q) (only parsing) : stdpp_scope.
+
+Notation "|={ E }â–·=> Q" := (|={E}[E]â–·=> Q)%I : bi_scope.
+Notation "P ={ E }▷=∗ Q" := (P ={E}[E]▷=∗ Q)%I : bi_scope.
+Notation "P ={ E }▷=∗ Q" := (P ={E}[E]▷=∗ Q) : stdpp_scope.
+
+(** For the iterated version, in principle there are 4 masks: "outer" and
+    "inner" of [|={Eo}[Ei]â–·=>], as well as "begin" and "end" masks [E1] and [E2]
+    that could potentially differ from [Eo]. The latter can be obtained from
+    this notation by adding normal mask-changing update modalities: [
+    |={E1,Eo}=> |={Eo}[Ei]â–·=>^n |={Eo,E2}=> Q] *)
+Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
+Notation "P ={ Eo } [ Ei ]▷=∗^ n Q" := (P -∗ |={Eo}[Ei]▷=>^n Q)%I : bi_scope.
+Notation "P ={ Eo } [ Ei ]▷=∗^ n Q" := (P -∗ |={Eo}[Ei]▷=>^n Q) (only parsing) : stdpp_scope.
+
+Notation "|={ E }â–·=>^ n Q" := (|={E}[E]â–·=>^n Q)%I : bi_scope.
+Notation "P ={ E }▷=∗^ n Q" := (P ={E}[E]▷=∗^n Q)%I : bi_scope.
+Notation "P ={ E }▷=∗^ n Q" := (P ={E}[E]▷=∗^n Q) (only parsing) : stdpp_scope.
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
@@ -324,39 +339,39 @@ Section fupd_derived.
   Proof. by rewrite (big_opMS_commute _). Qed.
 
   (** Fancy updates that take a step derived rules. *)
-  Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}▷=> P) -∗ (P -∗ Q) -∗ |={E1,E2,E3}▷=> Q.
+  Lemma step_fupd_wand Eo Ei P Q : (|={Eo}[Ei]▷=> P) -∗ (P -∗ Q) -∗ |={Eo}[Ei]▷=> Q.
   Proof.
     apply wand_intro_l.
     by rewrite (later_intro (P -∗ Q)%I) fupd_frame_l -later_sep fupd_frame_l
                wand_elim_l.
   Qed.
 
-  Lemma step_fupd_mask_frame_r E1 E2 E3 Ef P :
-    E1 ## Ef → E2 ## Ef → (|={E1,E2,E3}▷=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef,E3 ∪ Ef}▷=> P.
+  Lemma step_fupd_mask_frame_r Eo Ei Ef P :
+    Eo ## Ef → Ei ## Ef → (|={Eo}[Ei]▷=> P) ⊢ |={Eo ∪ Ef}[Ei ∪ Ef]▷=> P.
   Proof.
     intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply fupd_mask_frame_r.
   Qed.
 
-  Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
-    F1 ⊆ F2 → E1 ⊆ E2 → (|={E1,F2}▷=> P) ⊢ |={E2,F1}▷=> P.
+  Lemma step_fupd_mask_mono Eo1 Eo2 Ei1 Ei2 P :
+    Ei2 ⊆ Ei1 → Eo1 ⊆ Eo2 → (|={Eo1}[Ei1]▷=> P) ⊢ |={Eo2}[Ei2]▷=> P.
   Proof.
-    intros ??. rewrite -(emp_sep (|={E1,F2}â–·=> P)%I).
-    rewrite (fupd_intro_mask E2 E1 emp%I) //.
-    rewrite fupd_frame_r -(fupd_trans E2 E1 F1). f_equiv.
-    rewrite fupd_frame_l -(fupd_trans E1 F2 F1). f_equiv.
-    rewrite (fupd_intro_mask F2 F1 (|={_,_}=> emp)%I) //.
+    intros ??. rewrite -(emp_sep (|={Eo1}[Ei1]â–·=> P)%I).
+    rewrite (fupd_intro_mask Eo2 Eo1 emp%I) //.
+    rewrite fupd_frame_r -(fupd_trans Eo2 Eo1 Ei2). f_equiv.
+    rewrite fupd_frame_l -(fupd_trans Eo1 Ei1 Ei2). f_equiv.
+    rewrite (fupd_intro_mask Ei1 Ei2 (|={_,_}=> emp)%I) //.
     rewrite fupd_frame_r. f_equiv.
     rewrite [X in (X ∗ _)%I]later_intro -later_sep. f_equiv.
-    rewrite fupd_frame_r -(fupd_trans F1 F2 E2). f_equiv.
-    rewrite fupd_frame_l -(fupd_trans F2 E1 E2). f_equiv.
+    rewrite fupd_frame_r -(fupd_trans Ei2 Ei1 Eo2). f_equiv.
+    rewrite fupd_frame_l -(fupd_trans Ei1 Eo1 Eo2). f_equiv.
     by rewrite fupd_frame_r left_id.
   Qed.
 
-  Lemma step_fupd_intro E1 E2 P : E2 ⊆ E1 → ▷ P -∗ |={E1,E2}▷=> P.
-  Proof. intros. by rewrite -(step_fupd_mask_mono E2 _ _ E2) // -!fupd_intro. Qed.
+  Lemma step_fupd_intro Ei Eo P : Ei ⊆ Eo → ▷ P -∗ |={Eo}[Ei]▷=> P.
+  Proof. intros. by rewrite -(step_fupd_mask_mono Ei _ Ei _) // -!fupd_intro. Qed.
 
-  Lemma step_fupd_frame_l E1 E2 R Q :
-    (R ∗ |={E1, E2}▷=> Q) -∗ |={E1, E2}▷=> (R ∗ Q).
+  Lemma step_fupd_frame_l Eo Ei R Q :
+    (R ∗ |={Eo}[Ei]▷=> Q) -∗ |={Eo}[Ei]▷=> (R ∗ Q).
   Proof.
     rewrite fupd_frame_l.
     apply fupd_mono.
@@ -364,21 +379,21 @@ Section fupd_derived.
     by apply later_mono, fupd_mono.
   Qed.
 
-  Lemma step_fupd_fupd E E' P : (|={E,E'}▷=> P) ⊣⊢ (|={E,E'}▷=> |={E}=> P).
+  Lemma step_fupd_fupd Eo Ei P : (|={Eo}[Ei]▷=> P) ⊣⊢ (|={Eo}[Ei]▷=> |={Eo}=> P).
   Proof.
     apply (anti_symm (⊢)).
     - by rewrite -fupd_intro.
     - by rewrite fupd_trans.
   Qed.
 
-  Lemma step_fupdN_mono E1 E2 n P Q :
-    (P ⊢ Q) → (|={E1,E2}▷=>^n P) ⊢ (|={E1,E2}▷=>^n Q).
+  Lemma step_fupdN_mono Eo Ei n P Q :
+    (P ⊢ Q) → (|={Eo}[Ei]▷=>^n P) ⊢ (|={Eo}[Ei]▷=>^n Q).
   Proof.
     intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
   Qed.
 
-  Lemma step_fupdN_wand E1 E2 n P Q :
-    (|={E1,E2}▷=>^n P) -∗ (P -∗ Q) -∗ (|={E1,E2}▷=>^n Q).
+  Lemma step_fupdN_wand Eo Ei n P Q :
+    (|={Eo}[Ei]▷=>^n P) -∗ (P -∗ Q) -∗ (|={Eo}[Ei]▷=>^n Q).
   Proof.
     apply wand_intro_l. induction n as [|n IH]=> /=.
     { by rewrite wand_elim_l. }
@@ -387,14 +402,14 @@ Section fupd_derived.
   Qed.
 
   Lemma step_fupdN_S_fupd n E P:
-    (|={E, ∅}▷=>^(S n) P) ⊣⊢ (|={E, ∅}▷=>^(S n) |={E}=> P).
+    (|={E}[∅]▷=>^(S n) P) ⊣⊢ (|={E}[∅]▷=>^(S n) |={E}=> P).
   Proof.
     apply (anti_symm (⊢)); rewrite !Nat_iter_S_r; apply step_fupdN_mono;
       rewrite -step_fupd_fupd //.
   Qed.
 
-  Lemma step_fupdN_frame_l E1 E2 n R Q :
-    (R ∗ |={E1, E2}▷=>^n Q) -∗ |={E1, E2}▷=>^n (R ∗ Q).
+  Lemma step_fupdN_frame_l Eo Ei n R Q :
+    (R ∗ |={Eo}[Ei]▷=>^n Q) -∗ |={Eo}[Ei]▷=>^n (R ∗ Q).
   Proof.
     induction n as [|n IH]; simpl; [done|].
     rewrite step_fupd_frame_l IH //=.
@@ -465,13 +480,13 @@ Section fupd_derived.
       (|={E}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E}=> Φ x).
     Proof. by apply fupd_plain_forall. Qed.
 
-    Lemma step_fupd_plain E E' P `{!Plain P} : (|={E,E'}▷=> P) ={E}=∗ ▷ ◇ P.
+    Lemma step_fupd_plain Eo Ei P `{!Plain P} : (|={Eo}[Ei]▷=> P) ={Eo}=∗ ▷ ◇ P.
     Proof.
-      rewrite -(fupd_plain_mask _ E' (â–· â—‡ P)%I).
+      rewrite -(fupd_plain_mask _ Ei (â–· â—‡ P)%I).
       apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
     Qed.
 
-    Lemma step_fupdN_plain E E' n P `{!Plain P} : (|={E,E'}▷=>^n P) ={E}=∗ ▷^n ◇ P.
+    Lemma step_fupdN_plain Eo Ei n P `{!Plain P} : (|={Eo}[Ei]▷=>^n P) ={Eo}=∗ ▷^n ◇ P.
     Proof.
       induction n as [|n IH].
       - by rewrite -fupd_intro -except_0_intro.
@@ -481,16 +496,16 @@ Section fupd_derived.
         * by rewrite except_0_later.
     Qed.
 
-    Lemma step_fupd_plain_forall E1 E2 {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
-      E2 ⊆ E1 →
-      (|={E1,E2}▷=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1,E2}▷=> Φ x).
+    Lemma step_fupd_plain_forall Eo Ei {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
+      Ei ⊆ Eo →
+      (|={Eo}[Ei]▷=> ∀ x, Φ x) ⊣⊢ (∀ x, |={Eo}[Ei]▷=> Φ x).
     Proof.
       intros. apply (anti_symm _).
       { apply forall_intro=> x. by rewrite (forall_elim x). }
-      trans (∀ x, |={E1}=> ▷ ◇ Φ x)%I.
+      trans (∀ x, |={Eo}=> ▷ ◇ Φ x)%I.
       { apply forall_mono=> x. by rewrite step_fupd_plain. }
       rewrite -fupd_plain_forall'. apply fupd_elim.
-      rewrite -(fupd_except_0 E2 E1) -step_fupd_intro //.
+      rewrite -(fupd_except_0 Ei Eo) -step_fupd_intro //.
       by rewrite -later_forall -except_0_forall.
     Qed.
   End fupd_plainly_derived.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 52e256df15fe2c168e632db254c1f05aecb17aac..a2bcf4e653069722ec8fde488cac54c47b51653c 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -18,7 +18,7 @@ Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ fork_post }})%I.
 
 Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
-  state_interp σ1 (κ ++ κs) m -∗ WP e1 @ s; ⊤ {{ Φ }} ={⊤,∅}▷=∗
+  state_interp σ1 (κ ++ κs) m -∗ WP e1 @ s; ⊤ {{ Φ }} ={⊤}[∅]▷=∗
   state_interp σ2 κs (length efs + m) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s efs.
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
@@ -32,7 +32,7 @@ Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
   step (e1 :: t1,σ1) κ (t2, σ2) →
   state_interp σ1 (κ ++ κs) (length t1) -∗ WP e1 @ s; ⊤ {{ Φ }} -∗ wptp s t1 ==∗
   ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗
-  |={⊤,∅}▷=> state_interp σ2 κs (pred (length t2)) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2'.
+  |={⊤}[∅]▷=> state_interp σ2 κs (pred (length t2)) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2'.
 Proof.
   iIntros (Hstep) "Hσ He Ht".
   destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
@@ -52,7 +52,7 @@ Qed.
 Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   state_interp σ1 (κs ++ κs') (length t1) -∗ WP e1 @ s; ⊤ {{ Φ }} -∗ wptp s t1
-  ={⊤,∅}▷=∗^n ∃ e2 t2',
+  ={⊤}[∅]▷=∗^n ∃ e2 t2',
     ⌜t2 = e2 :: t2'⌝ ∗
     state_interp σ2 κs' (pred (length t2)) ∗
     WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2'.
@@ -80,7 +80,7 @@ Lemma wptp_strong_adequacy Φ κs' s n e1 t1 κs t2 σ1 σ2 :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   state_interp σ1 (κs ++ κs') (length t1) -∗
   WP e1 @ s; ⊤ {{ Φ }} -∗
-  wptp s t1 ={⊤,∅}▷=∗^(S n) ∃ e2 t2',
+  wptp s t1 ={⊤}[∅]▷=∗^(S n) ∃ e2 t2',
     ⌜ t2 = e2 :: t2' ⌝ ∗
     ⌜ ∀ e2, s = NotStuck → e2 ∈ t2 → not_stuck e2 σ2 ⌝ ∗
     state_interp σ2 κs' (length t2') ∗
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 1aa8577912251c5572013f0709419b5f95aaf792..7af252db44c1a8f7981a50943806cacffe078241 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -19,7 +19,7 @@ Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -70,7 +70,7 @@ Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -102,7 +102,7 @@ Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
       ⌜efs = []⌝ ∗ state_interp σ2 κs n ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
@@ -132,7 +132,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
     head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
-  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E}[E']▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2); eauto.
   destruct s; by auto.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index d7e657de4c36f1049dc1dc669aaaf96687a508b2..9a2d292e46e942b78e59f8a3bf3c57a5007bb9ea 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -20,7 +20,7 @@ Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
   (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
       state_interp σ2 κs (length efs + n) ∗
       WP e2 @ s; E {{ Φ }} ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -55,7 +55,7 @@ Qed.
 Lemma wp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E E' Φ e1 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
-  (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E {{ Φ }})
+  (|={E}[E']▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E {{ Φ }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
@@ -85,7 +85,7 @@ Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -123,7 +123,7 @@ Lemma wp_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E E' Φ} e1 e2 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
     κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
-  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E}[E']▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step_no_fork s E E'); try done.
   { naive_solver. }
@@ -134,7 +134,7 @@ Qed.
 Lemma wp_pure_step_fupd `{!Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
-  (|={E,E'}▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E}[E']▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
   iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 4e90d18c6c9860b14187adf913e06cfab3f00ecf..ec4ab9f47002fe3115cf7dbc5f4ae0e592d401e7 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -32,7 +32,7 @@ Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
   | None => ∀ σ1 κ κs n,
      state_interp σ1 (κ ++ κs) n ={E,∅}=∗
        ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-       ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
+       ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅,E}=>
          state_interp σ2 κs (length efs + n) ∗
          wp E e2 Φ ∗
          [∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
@@ -141,7 +141,7 @@ Qed.
 
 Lemma wp_step_fupd s E1 E2 e P Φ :
   TCEq (to_val e) None → E2 ⊆ E1 →
-  (|={E1,E2}▷=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; E1 {{ Φ }}.
+  (|={E1}[E2]▷=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; E1 {{ Φ }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
   iIntros (σ1 κ κs n) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
@@ -221,14 +221,14 @@ Proof. iIntros "[H ?]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
 
 Lemma wp_frame_step_l s E1 E2 e Φ R :
   TCEq (to_val e) None → E2 ⊆ E1 →
-  (|={E1,E2}▷=> R) ∗ WP e @ s; E2 {{ Φ }} ⊢ WP e @ s; E1 {{ v, R ∗ Φ v }}.
+  (|={E1}[E2]▷=> R) ∗ WP e @ s; E2 {{ Φ }} ⊢ WP e @ s; E1 {{ v, R ∗ Φ v }}.
 Proof.
   iIntros (??) "[Hu Hwp]". iApply (wp_step_fupd with "Hu"); try done.
   iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
 Qed.
 Lemma wp_frame_step_r s E1 E2 e Φ R :
   TCEq (to_val e) None → E2 ⊆ E1 →
-  WP e @ s; E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ WP e @ s; E1 {{ v, Φ v ∗ R }}.
+  WP e @ s; E2 {{ Φ }} ∗ (|={E1}[E2]▷=> R) ⊢ WP e @ s; E1 {{ v, Φ v ∗ R }}.
 Proof.
   rewrite [(WP _ @ _; _ {{ _ }} ∗ _)%I]comm; setoid_rewrite (comm _ _ R).
   apply wp_frame_step_l.
diff --git a/theories/proofmode/class_instances_updates.v b/theories/proofmode/class_instances_updates.v
index 3d9d0bf7d37fd6afc312597e60fba6d3dfe294ab..ddb4da903de55418f35497a2804d56113c111754 100644
--- a/theories/proofmode/class_instances_updates.v
+++ b/theories/proofmode/class_instances_updates.v
@@ -109,7 +109,7 @@ Global Instance from_forall_step_fupd
   (* Some cases in which [E2 ⊆ E1] holds *)
   TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
   FromForall P Φ → (∀ x, Plain (Φ x)) →
-  FromForall (|={E1,E2}▷=> P)%I (λ a, |={E1,E2}▷=> (Φ a))%I.
+  FromForall (|={E1}[E2]▷=> P)%I (λ a, |={E1}[E2]▷=> (Φ a))%I.
 Proof.
   rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
 Qed.