diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index b73514844349bab8cdf0eebe80b489ce11dec725..def2c522d6ffb9000783c1b26845a9f4c89075d4 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -62,6 +62,13 @@ Class BiEmbedFUpd (PROP1 PROP2 : sbi)
 Hint Mode BiEmbedFUpd - ! - - - : typeclass_instances.
 Hint Mode BiEmbedFUpd ! - - - - : typeclass_instances.
 
+Class BiEmbedPlainly (PROP1 PROP2 : sbi)
+      `{BiEmbed PROP1 PROP2, BiPlainly PROP1, BiPlainly PROP2} := {
+  embed_plainly_2 (P : PROP1) : ■ ⎡P⎤ ⊢ (⎡■ P⎤ : PROP2)
+}.
+Hint Mode BiEmbedPlainly - ! - - - : typeclass_instances.
+Hint Mode BiEmbedPlainly ! - - - - : typeclass_instances.
+
 Section embed_laws.
   Context `{BiEmbed PROP1 PROP2}.
   Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
@@ -270,6 +277,14 @@ Section sbi_embed.
   Lemma embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
   Proof. by rewrite embed_or embed_later embed_pure. Qed.
 
+  (* Not an instance, since it may cause overlap *)
+  Lemma bi_embed_plainly_emp `{!BiPlainly PROP1, !BiPlainly PROP2} :
+    BiEmbedEmp PROP1 PROP2 → BiEmbedPlainly PROP1 PROP2.
+  Proof.
+    intros. constructor=> P. rewrite !plainly_alt embed_internal_eq.
+    by rewrite -embed_affinely -embed_emp embed_interal_inj.
+  Qed.
+
   Lemma embed_plainly_1 `{!BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■ P⎤ ⊢ ■ ⎡P⎤.
   Proof.
     assert (∀ P, <affine> ⎡ P ⎤ ⊣⊢ (<affine> ⎡ <affine> P ⎤ : PROP2)) as Hhelp.
@@ -282,16 +297,14 @@ Section sbi_embed.
       - apply bi.and_intro; auto using embed_emp_2. }
     rewrite !plainly_alt embed_internal_eq. by rewrite Hhelp -Hemp -!bi.f_equiv.
   Qed.
-  Lemma embed_plainly `{!BiEmbedEmp PROP1 PROP2,
-    !BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤.
+  Lemma embed_plainly `{!BiPlainly PROP1, !BiPlainly PROP2,
+    !BiEmbedPlainly PROP1 PROP2} P : ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤.
   Proof.
-    apply (anti_symm _); first by apply embed_plainly_1.
-    rewrite !plainly_alt embed_internal_eq.
-    by rewrite -embed_affinely -embed_emp embed_interal_inj.
+    apply (anti_symm _). by apply embed_plainly_1. by apply embed_plainly_2.
   Qed.
 
-  Lemma embed_plainly_if `{!BiEmbedEmp PROP1 PROP2,
-    !BiPlainly PROP1, !BiPlainly PROP2} p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
+  Lemma embed_plainly_if `{!BiPlainly PROP1, !BiPlainly PROP2,
+    !BiEmbedPlainly PROP1 PROP2} p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
   Proof. destruct p; simpl; auto using embed_plainly. Qed.
   Lemma embed_plainly_if_1 `{!BiPlainly PROP1, !BiPlainly PROP2} p P :
     ⎡■?p P⎤ ⊢ ■?p ⎡P⎤.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index b94e69f60c4181565309cd838fa6ec6565f84f06..69e84c9d5fc4a294a66dedbd2b0587aab3eac10f 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -933,6 +933,10 @@ Proof.
   apply bi.forall_intro=>?. by do 2 f_equiv.
 Qed.
 
+Global Instance monPred_bi_embed_plainly `{BiPlainly PROP} :
+  BiEmbedPlainly PROP monPredSI.
+Proof. apply bi_embed_plainly_emp, _. Qed.
+
 Lemma monPred_plainly_unfold `{BiPlainly PROP} : plainly = λ P, ⎡ ∀ i, ■ (P i) ⎤%I.
 Proof. by rewrite monPred_plainly_eq monPred_embed_eq. Qed.
 Lemma monPred_at_plainly `{BiPlainly PROP} i P : (■ P) i ⊣⊢ ∀ j, ■ (P j).
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index adf0bc6990ebad99a297b803c44be9a475145a8d..f8045f913a86a255f4a6a412dc3a3796006a2f82 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -417,7 +417,7 @@ Global Instance from_modal_plainly `{BiPlainly PROP} P :
 Proof. by rewrite /FromModal. Qed.
 
 Global Instance from_modal_plainly_embed `{BiPlainly PROP, BiPlainly PROP',
-    BiEmbedEmp PROP PROP', !SbiEmbed PROP PROP'} `(sel : A) P Q :
+    BiEmbedPlainly PROP PROP', !SbiEmbed PROP PROP'} `(sel : A) P Q :
   FromModal modality_plainly sel P Q →
   FromModal modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
 Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.