diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 480faeda6efea6af5b9cc3cc24a70fd8422d6e36..574b84b39d629f23ddb310d98df217a8a1b07c41 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -172,6 +172,12 @@ Section bupd_derived_sbi.
       - rewrite -bupd_intro. apply forall_intro=> x.
         by rewrite (forall_elim x) bupd_plain.
     Qed.
+
+    Lemma bupd_plausibly P : (|==> P) ⊢ <plausible> P.
+    Proof.
+      apply forall_intro=> Q. apply wand_intro_l. rewrite bupd_frame_l.
+      by rewrite plainly_elim wand_elim_l bupd_plain.
+    Qed.
   End bupd_plainly.
 End bupd_derived_sbi.