diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index b6d0650377ccafa68e80b88602b3e5c1a0af2fac..5a6ef337eb350c2cd4ccf634f332510e256e6375 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -213,6 +213,8 @@ Lemma soundness_later P : bi_emp_valid (▷ P) → bi_emp_valid P.
 Proof. apply soundness_later. Qed.
 End restate.
 
+(** See [derived.v] for the version for basic updates. *)
+
 (** New unseal tactic that also unfolds the BI layer.
     This is used by [base_logic.double_negation].
     TODO: Can we get rid of this? *)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index e5b4462bd614ca47ec2c3469c6d2f7bf3dc3c8ce..7214311640a28474fb55f85cb852c550882e4f79 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -92,6 +92,12 @@ Global Instance uPred_ownM_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 
 (** Consistency/soundness statement *)
+Lemma soundness_bupd_plain P `{!Plain P} : bi_emp_valid (|==> P) → bi_emp_valid P.
+Proof.
+  eapply bi_emp_valid_mono. etrans; last exact: bupd_plainly. apply bupd_mono'.
+  apply: plain.
+Qed.
+
 Corollary soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
 Proof.
   induction n as [|n IH]=> /=.