diff --git a/CHANGELOG.md b/CHANGELOG.md
index 923b66e6f42ef476f01d425dda95bd43eecc2ff6..a755c1810174d94eabc1c067418a75c8fe0ae292 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -40,6 +40,7 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Add lemmas for swapping nested big-ops: `big_sep{L,M,S,MS}_sep{L,M,S,MS}`.
 * Rename `big_sep{L,L2,M,M2,S}_intuitionistically_forall` →
   `big_sep{L,L2,M,M2,S}_intro`, and `big_orL_lookup` → `big_orL_intro`.
+* Rename `bupd_forall` to `bupd_plain_forall`.
 
 **Changes in `proofmode`:**
 
@@ -102,6 +103,7 @@ s/\bbig_sepM2_lookup_2\b/big_sepM2_lookup_r/g
 # big_*_intro
 s/\bbig_sep(L|L2|M|M2|S)_intuitionistically_forall\b/big_sep\1_intro/g
 s/\bbig_orL_lookup\b/big_orL_intro/g
+s/\bbupd_forall\b/bupd_plain_forall/g
 EOF
 ```
 
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 00a97edb94b40ff527ac82df7a5aa7b52c70742a..afeaf0df073a619fcca3025fafa4ab483ad0c84b 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -230,7 +230,7 @@ Section bupd_derived.
     Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
     Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
 
-    Lemma bupd_forall {A} (Φ : A → PROP) `{∀ x, Plain (Φ x)} :
+    Lemma bupd_plain_forall {A} (Φ : A → PROP) `{∀ x, Plain (Φ x)} :
       (|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x).
     Proof.
       apply (anti_symm _).