diff --git a/CHANGELOG.md b/CHANGELOG.md
index af9fec9786db006d7662977d1bfde4e84999e2f7..210433e7f14c57aa0c403fae95931dc11d7f1f98 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -113,6 +113,8 @@ Coq 8.13 is no longer supported.
   `BiPersistentlyMixin`: Given a discrete BI that enjoys the existential
   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`
 
 **Changes in `proofmode`:**
 
@@ -202,6 +204,7 @@ s/\bfresh_locs(_fresh|)\b/Loc.fresh\1/g
 s/\bMonPred\.unseal\b/monPred\.unseal/g
 # big op
 s/\bbig_sepM2_alt\b/big_sepM2_alt_lookup/g
+s/\bbupd_plain\b/bupd_elim/g
 EOF
 ```
 
diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index 7e2abae22ac3986d1754eebe0136a0e756ccf3a0..335bd5a534be02e894f32323f1c90b7e1e718078 100644
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -125,7 +125,7 @@ Section derived.
   the empty context also without the modalities.
   For basic updates, soundness only holds for plain propositions. *)
   Lemma bupd_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
-  Proof. rewrite bupd_plain. done. Qed.
+  Proof. rewrite bupd_elim. done. Qed.
 
   Lemma laterN_soundness P n : (⊢ ▷^n P) → ⊢ P.
   Proof. induction n; eauto using later_soundness. Qed.
@@ -153,7 +153,7 @@ Section derived.
     move: H. apply bi_emp_valid_mono.
     induction ms as [|m ms IH]; first done; simpl.
     destruct m; simpl; rewrite IH.
-    - rewrite -later_intro. apply bupd_plain. apply _.
+    - rewrite -later_intro. apply bupd_elim. apply _.
     - done.
     - rewrite -later_intro persistently_elim. done.
     - rewrite -later_intro plainly_elim. done.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 4838a3cc147f184050903e9f1b043587d65444da..a75e7762df9338c37b54c89c4f1ae32989cbdcbd 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -253,7 +253,7 @@ Section bupd_derived.
   Section bupd_plainly.
     Context `{!BiPlainly PROP, !BiBUpdPlainly PROP}.
 
-    Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
+    Lemma bupd_elim P `{!Plain P} : (|==> P) ⊢ P.
     Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
 
     Lemma bupd_plain_forall {A} (Φ : A → PROP) `{∀ x, Plain (Φ x)} :
@@ -262,8 +262,15 @@ Section bupd_derived.
       apply (anti_symm _).
       - apply bupd_forall.
       - rewrite -bupd_intro. apply forall_intro=> x.
-        by rewrite (forall_elim x) bupd_plain.
+        by rewrite (forall_elim x) bupd_elim.
     Qed.
+
+    Global Instance bupd_plain P `{!Plain P} : Plain (|==> P).
+    Proof.
+      rewrite /Plain. rewrite {1}(plain P) {1}bupd_elim.
+      apply plainly_mono, bupd_intro.
+    Qed.
+
   End bupd_plainly.
 End bupd_derived.
 
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 76e318500dba8e7f85ccb43101656703a54d8df3..d182711d91999aa8314a2699f30ddf0ea7db2ccc 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -152,12 +152,12 @@ Global Instance elim_modal_bupd_plain_goal
   Plain Q → ElimModal True p false (|==> P) P Q Q.
 Proof.
   intros. by rewrite /ElimModal intuitionistically_if_elim
-    bupd_frame_r wand_elim_r bupd_plain.
+    bupd_frame_r wand_elim_r bupd_elim.
 Qed.
 Global Instance elim_modal_bupd_plain
     `{!BiBUpd PROP, !BiPlainly PROP, !BiBUpdPlainly PROP} p P Q :
   Plain P → ElimModal True p p (|==> P) P Q Q.
-Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
+Proof. intros. by rewrite /ElimModal bupd_elim wand_elim_r. Qed.
 Global Instance elim_modal_bupd_fupd
     `{!BiBUpd PROP, !BiFUpd PROP, !BiBUpdFUpd PROP} p E1 E2 P Q :
   ElimModal True p false (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.