diff --git a/CHANGELOG.md b/CHANGELOG.md
index 210433e7f14c57aa0c403fae95931dc11d7f1f98..75e7f9ccb7242ce76eaae354b55d25628baf99fe 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -114,7 +114,7 @@ Coq 8.13 is no longer supported.
   property, a trivial definition of the persistence modality can be given.
 * Fix `greatest_fixpoint_ne'` accidentally being about the least fixpoint.
 * Add `Plain` instance for `|==> P` when `P` is plain.
-  + Rename `bupd_plain` → `bupd_elim`
+* Rename `bupd_plain` → `bupd_elim`.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index a75e7762df9338c37b54c89c4f1ae32989cbdcbd..964b4567a7d8b3e865252e171927da89aa1a6504 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -265,10 +265,10 @@ Section bupd_derived.
         by rewrite (forall_elim x) bupd_elim.
     Qed.
 
-    Global Instance bupd_plain P `{!Plain P} : Plain (|==> P).
+    Global Instance bupd_plain P : Plain P → Plain (|==> P).
     Proof.
-      rewrite /Plain. rewrite {1}(plain P) {1}bupd_elim.
-      apply plainly_mono, bupd_intro.
+      intros. rewrite /Plain. rewrite {1}(plain P) {1}bupd_elim.
+      by rewrite -bupd_intro.
     Qed.
 
   End bupd_plainly.