diff --git a/CHANGELOG.md b/CHANGELOG.md
index 21375bfb0d0e78a504d5bc8a8b94b6bd96fec5c1..caee82ff7153e4c274b907bd51be0535d90cd195 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -208,7 +208,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * 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 lemma `step_fupd_mask_mono` now also has a more
+  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)
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 21813c140bbf13eac8508210db7b58460e726533..99599c3beb55ddbd5b91094c9b3349dbd87ff632 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -93,7 +93,7 @@ Reserved Notation "P ={ E }=∗ Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[' P  '/' ={ E }=∗  Q ']'").
 
-(** Step-taking updates *)
+(** Step-taking fancy updates *)
 Reserved Notation "|={ E1 } [ E2 ]â–·=> Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 } [ E2 ]â–·=>  Q").
@@ -107,7 +107,7 @@ Reserved Notation "P ={ E }▷=∗ Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[' P  '/' ={ E }▷=∗  Q ']'").
 
-(** Multi-step-taking updates *)
+(** 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").
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index dfe7fb75918f9dc12c430ed531ae1f547058ed93..9690d30af7ac1eadb9089a1d3a45c3fbdad672b7 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -26,12 +26,12 @@ 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. *)
+(** * Step-taking fancy updates. *)
 (** These have two masks, but they are different than the two masks of a
-    mask-changing update: the first mask ("outer mask") holds at the beginning
-    and the end, the second mask ("inner mask") holds around each â–·. This is
-    also why we use a different notation than for the two masks of a
-    mask-changing updates. *)
+    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.
@@ -40,12 +40,11 @@ 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 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]
-*)
+(** 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.