diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index f6b67352ed9df429c6691fd689df4d5a3a3ae4df..72f872b8100510e0ac3b8d35aaa26a02ee1301fc 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -815,6 +815,12 @@ Proof. intros. by rewrite /ElimModal persistently_elim wand_elim_r. Qed.
 Global Instance elim_modal_bupd P Q : ElimModal (|==> P) P (|==> Q) (|==> Q).
 Proof. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_trans. Qed.
 
+Global Instance elim_modal_bupd_plain_goal P Q : Plain Q → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_frame_r wand_elim_r bupd_plain. Qed.
+
+Global Instance elim_modal_bupd_plain P Q : Plain P → ElimModal (|==> P) P Q Q.
+Proof. intros. by rewrite /ElimModal bupd_plain wand_elim_r. Qed.
+
 Global Instance elim_modal_except_0 P Q : IsExcept0 Q → ElimModal (◇ P) P Q Q.
 Proof.
   intros. rewrite /ElimModal (except_0_intro (_ -∗ _)).