diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index ee071f187b83628a4e13ce37317cab77b646368f..4201349f1703af21d348286ce1acc84704fd1a5a 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -15,8 +15,9 @@ Hint Mode Embed - ! : typeclass_instances.
 Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
   bi_embed_mixin_ne : NonExpansive embed;
   bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) embed;
-  bi_embed_mixin_entails_inj :> Inj (⊢) (⊢) embed;
-  bi_embed_mixin_emp : ⎡emp⎤ ⊣⊢ emp;
+  bi_embed_mixin_emp_valid_inj (P : PROP1) :
+    bi_emp_valid (PROP:=PROP2) ⎡P⎤ → bi_emp_valid P;
+  bi_embed_mixin_emp_2 : emp ⊢ ⎡emp⎤;
   bi_embed_mixin_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤;
   bi_embed_mixin_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤;
   bi_embed_mixin_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤;
@@ -33,6 +34,12 @@ Hint Mode BiEmbed ! - : typeclass_instances.
 Hint Mode BiEmbed - ! : typeclass_instances.
 Arguments bi_embed_embed : simpl never.
 
+Class BiEmbedEmp (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := {
+  embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp;
+}.
+Hint Mode BiEmbedEmp ! - - : typeclass_instances.
+Hint Mode BiEmbedEmp - ! - : typeclass_instances.
+
 Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
   embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y;
   embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤;
@@ -55,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)).
@@ -65,10 +79,10 @@ Section embed_laws.
   Proof. eapply bi_embed_mixin_ne, bi_embed_mixin. Qed.
   Global Instance embed_mono : Proper ((⊢) ==> (⊢)) embed.
   Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed.
-  Global Instance embed_entails_inj : Inj (⊢) (⊢) embed.
-  Proof. eapply bi_embed_mixin_entails_inj, bi_embed_mixin. Qed.
-  Lemma embed_emp : ⎡emp⎤ ⊣⊢ emp.
-  Proof. eapply bi_embed_mixin_emp, bi_embed_mixin. Qed.
+  Lemma embed_emp_valid_inj P : (⎡P⎤ : PROP2)%I → P.
+  Proof. eapply bi_embed_mixin_emp_valid_inj, bi_embed_mixin. Qed.
+  Lemma embed_emp_2 : emp ⊢ ⎡emp⎤.
+  Proof. eapply bi_embed_mixin_emp_2, bi_embed_mixin. Qed.
   Lemma embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤.
   Proof. eapply bi_embed_mixin_impl_2, bi_embed_mixin. Qed.
   Lemma embed_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤.
@@ -93,17 +107,27 @@ Section embed.
   Proof. apply (ne_proper _). Qed.
   Global Instance embed_flip_mono : Proper (flip (⊢) ==> flip (⊢)) embed.
   Proof. solve_proper. Qed.
+  Global Instance embed_entails_inj : Inj (⊢) (⊢) embed.
+  Proof.
+    move=> P Q /bi.entails_wand. rewrite embed_wand_2.
+    by move=> /embed_emp_valid_inj /bi.wand_entails.
+  Qed.
+
   Global Instance embed_inj : Inj (≡) (≡) embed.
   Proof.
-    intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed);
-    rewrite EQ //.
+    intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed); rewrite EQ //.
   Qed.
 
   Lemma embed_emp_valid (P : PROP1) : ⎡P⎤%I ↔ P.
   Proof.
-    by rewrite /bi_emp_valid -embed_emp; split=>?; [apply (inj embed)|f_equiv].
+    rewrite /bi_emp_valid. split=> HP.
+    - by apply embed_emp_valid_inj.
+    - by rewrite embed_emp_2 HP.
   Qed.
 
+  Lemma embed_emp `{!BiEmbedEmp PROP1 PROP2} : ⎡ emp ⎤ ⊣⊢ emp.
+  Proof. apply (anti_symm _); eauto using embed_emp_1, embed_emp_2. Qed.
+
   Lemma embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
   Proof.
     apply bi.equiv_spec; split; [|apply embed_forall_2].
@@ -141,18 +165,30 @@ Section embed.
   Proof. by rewrite embed_and !embed_impl. Qed.
   Lemma embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤).
   Proof. by rewrite embed_and !embed_wand. Qed.
-  Lemma embed_affinely P : ⎡<affine> P⎤ ⊣⊢ <affine> ⎡P⎤.
-  Proof. by rewrite embed_and embed_emp. Qed.
+  Lemma embed_affinely_2 P : <affine> ⎡P⎤ ⊢ ⎡<affine> P⎤.
+  Proof. by rewrite embed_and -embed_emp_2. Qed.
+  Lemma embed_affinely `{!BiEmbedEmp PROP1 PROP2} P : ⎡<affine> P⎤ ⊣⊢ <affine> ⎡P⎤.
+  Proof. by rewrite /bi_intuitionistically embed_and embed_emp. Qed.
   Lemma embed_absorbingly P : ⎡<absorb> P⎤ ⊣⊢ <absorb> ⎡P⎤.
   Proof. by rewrite embed_sep embed_pure. Qed.
-  Lemma embed_intuitionistically P : ⎡□ P⎤ ⊣⊢ □ ⎡P⎤.
-  Proof. rewrite embed_and embed_emp embed_persistently //. Qed.
+  Lemma embed_intuitionistically_2 P : □ ⎡P⎤ ⊢ ⎡□ P⎤.
+  Proof. by rewrite /bi_intuitionistically -embed_affinely_2 embed_persistently. Qed.
+  Lemma embed_intuitionistically `{!BiEmbedEmp PROP1 PROP2} P : ⎡□ P⎤ ⊣⊢ □ ⎡P⎤.
+  Proof. by rewrite /bi_intuitionistically embed_affinely embed_persistently. Qed.
+
   Lemma embed_persistently_if P b : ⎡<pers>?b P⎤ ⊣⊢ <pers>?b ⎡P⎤.
   Proof. destruct b; simpl; auto using embed_persistently. Qed.
-  Lemma embed_affinely_if P b : ⎡<affine>?b P⎤ ⊣⊢ <affine>?b ⎡P⎤.
+  Lemma embed_affinely_if_2 P b : <affine>?b ⎡P⎤ ⊢ ⎡<affine>?b P⎤.
+  Proof. destruct b; simpl; auto using embed_affinely_2. Qed.
+  Lemma embed_affinely_if `{!BiEmbedEmp PROP1 PROP2} P b :
+    ⎡<affine>?b P⎤ ⊣⊢ <affine>?b ⎡P⎤.
   Proof. destruct b; simpl; auto using embed_affinely. Qed.
-  Lemma embed_intuitionistically_if P b : ⎡□?b P⎤ ⊣⊢ □?b ⎡P⎤.
+  Lemma embed_intuitionistically_if_2 P b : □?b ⎡P⎤ ⊢ ⎡□?b P⎤.
+  Proof. destruct b; simpl; auto using embed_intuitionistically_2. Qed.
+  Lemma embed_intuitionistically_if `{!BiEmbedEmp PROP1 PROP2} P b :
+    ⎡□?b P⎤ ⊣⊢ □?b ⎡P⎤.
   Proof. destruct b; simpl; auto using embed_intuitionistically. Qed.
+
   Lemma embed_hforall {As} (Φ : himpl As PROP1):
     ⎡bi_hforall Φ⎤ ⊣⊢ bi_hforall (hcompose embed Φ).
   Proof. induction As=>//. rewrite /= embed_forall. by do 2 f_equiv. Qed.
@@ -162,7 +198,7 @@ Section embed.
 
   Global Instance embed_persistent P : Persistent P → Persistent ⎡P⎤.
   Proof. intros ?. by rewrite /Persistent -embed_persistently -persistent. Qed.
-  Global Instance embed_affine P : Affine P → Affine ⎡P⎤.
+  Global Instance embed_affine `{!BiEmbedEmp PROP1 PROP2} P : Affine P → Affine ⎡P⎤.
   Proof. intros ?. by rewrite /Affine (affine P) embed_emp. Qed.
   Global Instance embed_absorbing P : Absorbing P → Absorbing ⎡P⎤.
   Proof. intros ?. by rewrite /Absorbing -embed_absorbingly absorbing. Qed.
@@ -179,25 +215,50 @@ Section embed.
     by split; [split|]; try apply _;
       [setoid_rewrite embed_or|rewrite embed_pure].
   Qed.
-  Global Instance embed_sep_homomorphism :
-    MonoidHomomorphism bi_sep bi_sep (≡) embed.
+
+  Global Instance embed_sep_entails_homomorphism :
+    MonoidHomomorphism bi_sep bi_sep (flip (⊢)) embed.
   Proof.
-    by split; [split|]; try apply _;
-      [setoid_rewrite embed_sep|rewrite embed_emp].
-  Qed.
-
-  Lemma embed_big_sepL {A} (Φ : nat → A → PROP1) l :
-    ⎡[∗ list] k↦x ∈ l, Φ k x⎤ ⊣⊢ [∗ list] k↦x ∈ l, ⎡Φ k x⎤.
-  Proof. apply (big_opL_commute _). Qed.
-  Lemma embed_big_sepM `{Countable K} {A} (Φ : K → A → PROP1) (m : gmap K A) :
-    ⎡[∗ map] k↦x ∈ m, Φ k x⎤ ⊣⊢ [∗ map] k↦x ∈ m, ⎡Φ k x⎤.
-  Proof. apply (big_opM_commute _). Qed.
-  Lemma embed_big_sepS `{Countable A} (Φ : A → PROP1) (X : gset A) :
-    ⎡[∗ set] y ∈ X, Φ y⎤ ⊣⊢ [∗ set] y ∈ X, ⎡Φ y⎤.
-  Proof. apply (big_opS_commute _). Qed.
-  Lemma embed_big_sepMS `{Countable A} (Φ : A → PROP1) (X : gmultiset A) :
-    ⎡[∗ mset] y ∈ X, Φ y⎤ ⊣⊢ [∗ mset] y ∈ X, ⎡Φ y⎤.
-  Proof. apply (big_opMS_commute _). Qed.
+    split; [split|]; simpl; try apply _;
+      [by setoid_rewrite embed_sep|by rewrite embed_emp_2].
+  Qed.
+
+  Lemma embed_big_sepL_2 {A} (Φ : nat → A → PROP1) l :
+    ([∗ list] k↦x ∈ l, ⎡Φ k x⎤) ⊢ ⎡[∗ list] k↦x ∈ l, Φ k x⎤.
+  Proof. apply (big_opL_commute (R:=flip (⊢)) _). Qed.
+  Lemma embed_big_sepM_2 `{Countable K} {A} (Φ : K → A → PROP1) (m : gmap K A) :
+    ([∗ map] k↦x ∈ m, ⎡Φ k x⎤) ⊢ ⎡[∗ map] k↦x ∈ m, Φ k x⎤.
+  Proof. apply (big_opM_commute (R:=flip (⊢)) _). Qed.
+  Lemma embed_big_sepS_2 `{Countable A} (Φ : A → PROP1) (X : gset A) :
+    ([∗ set] y ∈ X, ⎡Φ y⎤) ⊢ ⎡[∗ set] y ∈ X, Φ y⎤.
+  Proof. apply (big_opS_commute (R:=flip (⊢)) _). Qed.
+  Lemma embed_big_sepMS_2 `{Countable A} (Φ : A → PROP1) (X : gmultiset A) :
+    ([∗ mset] y ∈ X, ⎡Φ y⎤) ⊢ ⎡[∗ mset] y ∈ X, Φ y⎤.
+  Proof. apply (big_opMS_commute (R:=flip (⊢)) _). Qed.
+
+  Section big_ops_emp.
+    Context `{!BiEmbedEmp PROP1 PROP2}.
+
+    Global Instance embed_sep_homomorphism :
+      MonoidHomomorphism bi_sep bi_sep (≡) embed.
+    Proof.
+      by split; [split|]; try apply _;
+        [setoid_rewrite embed_sep|rewrite embed_emp].
+    Qed.
+
+    Lemma embed_big_sepL {A} (Φ : nat → A → PROP1) l :
+      ⎡[∗ list] k↦x ∈ l, Φ k x⎤ ⊣⊢ [∗ list] k↦x ∈ l, ⎡Φ k x⎤.
+    Proof. apply (big_opL_commute _). Qed.
+    Lemma embed_big_sepM `{Countable K} {A} (Φ : K → A → PROP1) (m : gmap K A) :
+      ⎡[∗ map] k↦x ∈ m, Φ k x⎤ ⊣⊢ [∗ map] k↦x ∈ m, ⎡Φ k x⎤.
+    Proof. apply (big_opM_commute _). Qed.
+    Lemma embed_big_sepS `{Countable A} (Φ : A → PROP1) (X : gset A) :
+      ⎡[∗ set] y ∈ X, Φ y⎤ ⊣⊢ [∗ set] y ∈ X, ⎡Φ y⎤.
+    Proof. apply (big_opS_commute _). Qed.
+    Lemma embed_big_sepMS `{Countable A} (Φ : A → PROP1) (X : gmultiset A) :
+      ⎡[∗ mset] y ∈ X, Φ y⎤ ⊣⊢ [∗ mset] y ∈ X, ⎡Φ y⎤.
+    Proof. apply (big_opMS_commute _). Qed.
+  End big_ops_emp.
 End embed.
 
 Section sbi_embed.
@@ -216,17 +277,41 @@ Section sbi_embed.
   Lemma embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
   Proof. by rewrite embed_or embed_later embed_pure. Qed.
 
-  Lemma embed_plainly `{!BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤.
+  (* Not an instance, since it may cause overlap *)
+  Lemma bi_embed_plainly_emp `{!BiPlainly PROP1, !BiPlainly PROP2} :
+    BiEmbedEmp PROP1 PROP2 → BiEmbedPlainly PROP1 PROP2.
   Proof.
-    rewrite !plainly_alt embed_internal_eq. apply (anti_symm _).
-    - rewrite -embed_affinely -embed_emp. apply bi.f_equiv, _.
-    - by rewrite -embed_affinely -embed_emp embed_interal_inj.
+    intros. constructor=> P. rewrite !plainly_alt embed_internal_eq.
+    by rewrite -embed_affinely -embed_emp embed_interal_inj.
   Qed.
-  Lemma embed_plainly_if `{!BiPlainly PROP1, !BiPlainly PROP2} p P : ⎡■?p P⎤ ⊣⊢ ■?p ⎡P⎤.
+
+  Lemma embed_plainly_1 `{!BiPlainly PROP1, !BiPlainly PROP2} P : ⎡■ P⎤ ⊢ ■ ⎡P⎤.
+  Proof.
+    assert (∀ P, <affine> ⎡ P ⎤ ⊣⊢ (<affine> ⎡ <affine> P ⎤ : PROP2)) as Hhelp.
+    { intros P'. apply (anti_symm _).
+      - by rewrite -bi.affinely_idemp (embed_affinely_2 P').
+      - by rewrite (bi.affinely_elim P'). }
+    assert (<affine> ⎡ emp ⎤ ⊣⊢ (emp : PROP2)) as Hemp.
+    { apply (anti_symm _).
+      - apply bi.affinely_elim_emp.
+      - 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 `{!BiPlainly PROP1, !BiPlainly PROP2,
+    !BiEmbedPlainly PROP1 PROP2} P : ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤.
+  Proof.
+    apply (anti_symm _). by apply embed_plainly_1. by apply embed_plainly_2.
+  Qed.
+
+  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⎤.
+  Proof. destruct p; simpl; auto using embed_plainly_1. Qed.
 
   Lemma embed_plain `{!BiPlainly PROP1, !BiPlainly PROP2} P : Plain P → Plain ⎡P⎤.
-  Proof. intros ?. by rewrite /Plain -embed_plainly -plain. Qed.
+  Proof. intros ?. by rewrite /Plain {1}(plain P) embed_plainly_1. Qed.
 
   Global Instance embed_timeless P : Timeless P → Timeless ⎡P⎤.
   Proof.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 4e0df1b95d65efe7085bfc9cbe4ce19694a9f4df..828bf4eb0e0d8d4580c752ed1e01b3ced00ecddf 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -411,15 +411,17 @@ Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed.
 
 Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
 Proof.
-  split; try apply _; unseal; try done.
-  - move =>?? /= [/(_ inhabitant) ?] //.
-  - split=>? /=.
+  split; try apply _; rewrite /bi_emp_valid; unseal; try done.
+  - move=> P /= [/(_ inhabitant) ?] //.
+  - intros P Q. split=> i /=.
     by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
-  - split=>? /=.
+  - intros P Q. split=> i /=.
     by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
 Qed.
 Global Instance monPred_bi_embed : BiEmbed PROP monPredI :=
   {| bi_embed_mixin := monPred_embedding_mixin |}.
+Global Instance monPred_bi_embed_emp : BiEmbedEmp PROP monPredI.
+Proof. split. by unseal. Qed.
 
 Lemma monPred_emp_unfold : emp%I = ⎡emp : PROP⎤%I.
 Proof. by unseal. Qed.
@@ -936,6 +938,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_bi.v b/theories/proofmode/class_instances_bi.v
index 2696a0e3d83808b469140265f4187aa7a90860d7..e431e99a6dd829116fc40c3b6a34838f3807c3d4 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -215,7 +215,7 @@ Global Instance from_pure_absorbingly P φ :
 Proof. rewrite /FromPure=> <- /=. by rewrite persistent_absorbingly_affinely. Qed.
 Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
   FromPure a P φ → FromPure a ⎡P⎤ φ.
-Proof. rewrite /FromPure=> <-. by rewrite embed_affinely_if embed_pure. Qed.
+Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
 
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
@@ -281,7 +281,7 @@ Proof. by rewrite /FromModal /= =><-. Qed.
 Global Instance from_modal_affinely_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
   FromModal modality_affinely sel P Q →
   FromModal modality_affinely sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely. Qed.
+Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely_2. Qed.
 Global Instance from_modal_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
   FromModal modality_persistently sel P Q →
   FromModal modality_persistently sel ⎡P⎤ ⎡Q⎤ | 100.
@@ -289,9 +289,7 @@ Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
 Global Instance from_modal_intuitionistically_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
   FromModal modality_intuitionistically sel P Q →
   FromModal modality_intuitionistically sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof.
-  rewrite /FromModal /= =><-. by rewrite embed_affinely embed_persistently.
-Qed.
+Proof. rewrite /FromModal /= =><-. by rewrite embed_intuitionistically_2. Qed.
 
 (* IntoWand *)
 Global Instance into_wand_wand p q P Q P' :
@@ -364,9 +362,7 @@ Global Instance into_wand_persistently_false q R P Q :
 Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
 Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q :
   IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
-Proof.
-  rewrite /IntoWand -!embed_intuitionistically_if -embed_wand => -> //.
-Qed.
+Proof. by rewrite /IntoWand !embed_intuitionistically_if_2 -embed_wand=> ->. Qed.
 
 (* FromWand *)
 Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
@@ -517,7 +513,8 @@ Qed.
 Global Instance into_and_embed `{BiEmbed PROP PROP'} p P Q1 Q2 :
   IntoAnd p P Q1 Q2 → IntoAnd p ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
 Proof.
-  rewrite /IntoAnd -embed_and -!embed_intuitionistically_if=> -> //.
+  rewrite /IntoAnd -embed_and=> HP. apply intuitionistically_if_intro'.
+  by rewrite embed_intuitionistically_if_2 HP intuitionistically_if_elim.
 Qed.
 
 (* IntoSep *)
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 9ae1b1d9583d1ea3b7f01ad5e14a0cb54c4b2a62..78b7091f7fb0666bdfe6b25b189f183a324d3933 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -416,8 +416,8 @@ Global Instance from_modal_plainly `{BiPlainly PROP} P :
   FromModal modality_plainly (â–  P) (â–  P) P | 2.
 Proof. by rewrite /FromModal. Qed.
 
-Global Instance from_modal_plainly_embed
-    `{BiPlainly PROP, BiPlainly PROP', SbiEmbed PROP PROP'} `(sel : A) P Q :
+Global Instance from_modal_plainly_embed `{BiPlainly PROP, BiPlainly PROP',
+    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.
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 6326f2763403f87bcdff83bf489e4a1777bd3b57..387608462e5f3c803b7473b8b0769490978adfad 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -35,7 +35,7 @@ Qed.
 Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
   KnownMakeEmbed ⌜φ⌝ ⌜φ⌝.
 Proof. apply embed_pure. Qed.
-Global Instance make_embed_emp `{BiEmbed PROP PROP'} :
+Global Instance make_embed_emp `{BiEmbedEmp PROP PROP'} :
   KnownMakeEmbed emp emp.
 Proof. apply embed_emp. Qed.
 Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
@@ -46,7 +46,7 @@ Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
   Frame p R P Q → MakeEmbed Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
 Proof.
   rewrite /Frame /MakeEmbed => <- <-.
-  rewrite embed_sep embed_intuitionistically_if => //.
+  rewrite embed_sep embed_intuitionistically_if_2 => //.
 Qed.
 Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
   Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' → Frame p ⌜φ⌝ ⎡P⎤ Q'.
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
index 6018b7aaee6f7ebd95ae9b71236a8d7601ad1862..2cb4571d58079a36b9aae058a7e4025d6e73718d 100644
--- a/theories/proofmode/modality_instances.v
+++ b/theories/proofmode/modality_instances.v
@@ -39,9 +39,8 @@ Section bi_modalities.
       (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
   Proof.
     split; simpl; split_and?;
-      eauto using equiv_entails_sym, embed_emp, embed_sep, embed_and.
-    - intros P Q. rewrite /IntoEmbed=> ->.
-      by rewrite embed_affinely embed_persistently.
+      eauto using equiv_entails_sym, embed_emp_2, embed_sep, embed_and.
+    - intros P Q. rewrite /IntoEmbed=> ->. by rewrite embed_intuitionistically_2.
     - by intros P Q ->.
   Qed.
   Definition modality_embed `{BiEmbed PROP PROP'} :=