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..b4c6d87ca1285ed3c248be4b73bfaa7ee5c1c680 100644
--- a/theories/bi/ascii.v
+++ b/theories/bi/ascii.v
@@ -89,24 +89,24 @@ 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
+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..6b2123c32e31d87d0fef5f353f322cbb8de30f75 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -99,24 +99,31 @@ Reserved Notation "|={ E1 , E2 , E3 }â–·=> Q"
 Reserved Notation "P ={ E1 , E2 , E3 }â–·=âˆ— Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "'[' P  '/' ={ E1 , E2 , E3 }â–·=âˆ—  Q ']'").
-Reserved Notation "|={ E1 , E2 }â–·=> 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"
+   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"
+
+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..98cead792b108bd52f4f29b8777bc949ba984427 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -26,17 +26,38 @@ 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. *)
+(** * Fancy updates that take a step. *)
+(** These have three masks: one they start with, one that is active when the step
+    is taken, and one they and with.*)
 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.
+Notation "P ={ E1 , E2 , E3 }â–·=âˆ— Q" := (P -âˆ— |={ E1,E2,E3 }â–·=> Q) (only parsing) : stdpp_scope.
+
+(** Often, the first and last mask are the same, so we just have two massk:
+    the "outer" one active at the beginning/end, and the "inner" one active
+    for each step. We avoid the "," here as that looks like a mask-changing update,
+    but this update really starts and ends at E1. *)
+Notation "|={ E1 } [ E2 ]â–·=> Q" := (|={E1,E2,E1}â–·=> Q)%I : bi_scope.
+Notation "P ={ E1 } [ E2 ]â–·=âˆ— Q" := (P -âˆ— |={ E1 , E2, E1 }â–·=> Q)%I : bi_scope.
+Notation "P ={ E1 } [ E2 ]â–·=âˆ— Q" := (P -âˆ— |={ E1 , E2, E1 }â–·=> 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 [|={E1}[E2]â–·=>], as well as a potentially
+    different "begin" and "end" mask. The latter can be obtained from
+    this notation by adding normal mask-changing update modalities:
+    [ |={Ebegin,Eouter}=> |={Eouter}[Einner]â–·=>^n |={Eouter,Eend}=> Q]
+*)
+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 : bi_scope.
+Notation "P ={ E1 } [ E2 ]â–·=âˆ—^ n Q" := (P -âˆ— |={E1}[E2]â–·=>^n Q) (only parsing) : stdpp_scope.
+
+Notation "|={ E1 }â–·=>^ n Q" := (|={E1}[E1]â–·=>^n Q)%I : bi_scope.
+Notation "P ={ E1 }â–·=âˆ—^ n Q" := (P ={E1}[E1]â–·=âˆ—^n Q)%I : bi_scope.
+Notation "P ={ E1 }â–·=âˆ—^ n Q" := (P ={E1}[E1]â–·=âˆ—^n Q) (only parsing) : stdpp_scope.
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
@@ -338,9 +359,9 @@ Section fupd_derived.
   Qed.
 
   Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
-    F1 âŠ† F2 â†’ E1 âŠ† E2 â†’ (|={E1,F2}â–·=> P) âŠ¢ |={E2,F1}â–·=> P.
+    F1 âŠ† F2 â†’ E1 âŠ† E2 â†’ (|={E1}[F2]â–·=> P) âŠ¢ |={E2}[F1]â–·=> P.
   Proof.
-    intros ??. rewrite -(emp_sep (|={E1,F2}â–·=> P)%I).
+    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.
@@ -352,11 +373,11 @@ Section fupd_derived.
     by rewrite fupd_frame_r left_id.
   Qed.
 
-  Lemma step_fupd_intro E1 E2 P : E2 âŠ† E1 â†’ â–· P -âˆ— |={E1,E2}â–·=> P.
+  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_frame_l E1 E2 R Q :
-    (R âˆ— |={E1, E2}â–·=> Q) -âˆ— |={E1, E2}â–·=> (R âˆ— Q).
+    (R âˆ— |={E1}[E2]â–·=> Q) -âˆ— |={E1}[E2]â–·=> (R âˆ— Q).
   Proof.
     rewrite fupd_frame_l.
     apply fupd_mono.
@@ -364,7 +385,7 @@ 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 E E' P : (|={E}[E']â–·=> P) âŠ£âŠ¢ (|={E}[E']â–·=> |={E}=> P).
   Proof.
     apply (anti_symm (âŠ¢)).
     - by rewrite -fupd_intro.
@@ -372,13 +393,13 @@ Section fupd_derived.
   Qed.
 
   Lemma step_fupdN_mono E1 E2 n P Q :
-    (P âŠ¢ Q) â†’ (|={E1,E2}â–·=>^n P) âŠ¢ (|={E1,E2}â–·=>^n Q).
+    (P âŠ¢ Q) â†’ (|={E1}[E2]â–·=>^n P) âŠ¢ (|={E1}[E2]â–·=>^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).
+    (|={E1}[E2]â–·=>^n P) -âˆ— (P -âˆ— Q) -âˆ— (|={E1}[E2]â–·=>^n Q).
   Proof.
     apply wand_intro_l. induction n as [|n IH]=> /=.
     { by rewrite wand_elim_l. }
@@ -387,14 +408,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).
+    (R âˆ— |={E1}[E2]â–·=>^n Q) -âˆ— |={E1}[E2]â–·=>^n (R âˆ— Q).
   Proof.
     induction n as [|n IH]; simpl; [done|].
     rewrite step_fupd_frame_l IH //=.
@@ -465,13 +486,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 E E' P `{!Plain P} : (|={E}[E']â–·=> P) ={E}=âˆ— â–· â—‡ P.
     Proof.
       rewrite -(fupd_plain_mask _ E' (â–· â—‡ 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 E E' n P `{!Plain P} : (|={E}[E']â–·=>^n P) ={E}=âˆ— â–·^n â—‡ P.
     Proof.
       induction n as [|n IH].
       - by rewrite -fupd_intro -except_0_intro.
@@ -483,7 +504,7 @@ Section fupd_derived.
 
     Lemma step_fupd_plain_forall E1 E2 {A} (Î¦ : A â†’ PROP) `{!âˆ€ x, Plain (Î¦ x)} :
       E2 âŠ† E1 â†’
-      (|={E1,E2}â–·=> âˆ€ x, Î¦ x) âŠ£âŠ¢ (âˆ€ x, |={E1,E2}â–·=> Î¦ x).
+      (|={E1}[E2]â–·=> âˆ€ x, Î¦ x) âŠ£âŠ¢ (âˆ€ x, |={E1}[E2]â–·=> Î¦ x).
     Proof.
       intros. apply (anti_symm _).
       { apply forall_intro=> x. by rewrite (forall_elim x). }
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..f2d08c6955768b6535cfdd8742333331ab50fc75 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -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..5d895d6ec1e8816b0a4adbee5983c8ee071f9e1b 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -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..f5ed45646d39ea97ed359b104fc00c1c290f1864 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -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.