diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 635d39dc309c2e987f6cc96275efc176bd1a2245..957a827d902cd0fd9488d5f2a4f36dc081bcac3a 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -2,173 +2,207 @@ From iris.algebra Require Import monoid.
 From iris.bi Require Import interface derived_laws big_op.
 From stdpp Require Import hlist.
 
-(* Embeddings are often used to *define* the connectives of the
-   domain BI. Hence we cannot ask it to verify the properties of
-   embeddings. *)
-Class BiEmbed (A B : Type) := bi_embed : A → B.
-Arguments bi_embed {_ _ _} _%I : simpl never.
-Notation "⎡ P ⎤" := (bi_embed P) : bi_scope.
-Instance: Params (@bi_embed) 3.
-Typeclasses Opaque bi_embed.
+Class Embed (A B : Type) := embed : A → B.
+Arguments embed {_ _ _} _%I : simpl never.
+Notation "⎡ P ⎤" := (embed P) : bi_scope.
+Instance: Params (@embed) 3.
+Typeclasses Opaque embed.
 
+Hint Mode Embed ! - : typeclass_instances.
+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_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⎤;
+  bi_embed_mixin_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤;
+  bi_embed_mixin_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤;
+  bi_embed_mixin_plainly P : ⎡bi_plainly P⎤ ⊣⊢ bi_plainly ⎡P⎤;
+  bi_embed_mixin_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤
+}.
+
+Class BiEmbed (PROP1 PROP2 : bi) := {
+  bi_embed_embed :> Embed PROP1 PROP2;
+  bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed;
+}.
 Hint Mode BiEmbed ! - : typeclass_instances.
 Hint Mode BiEmbed - ! : typeclass_instances.
+Arguments bi_embed_embed : simpl never.
 
-Class BiEmbedding (PROP1 PROP2 : bi) `{BiEmbed PROP1 PROP2} := {
-  bi_embed_ne :> NonExpansive bi_embed;
-  bi_embed_mono :> Proper ((⊢) ==> (⊢)) bi_embed;
-  bi_embed_entails_inj :> Inj (⊢) (⊢) bi_embed;
-  bi_embed_emp : ⎡emp⎤ ⊣⊢ emp;
-  bi_embed_impl_2 P Q : (⎡P⎤ → ⎡Q⎤) ⊢ ⎡P → Q⎤;
-  bi_embed_forall_2 A (Φ : A → PROP1) : (∀ x, ⎡Φ x⎤) ⊢ ⎡∀ x, Φ x⎤;
-  bi_embed_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤;
-  bi_embed_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤;
-  bi_embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤;
-  bi_embed_plainly P : ⎡bi_plainly P⎤ ⊣⊢ bi_plainly ⎡P⎤;
-  bi_embed_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤
+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⎤
 }.
 
-Class SbiEmbedding (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
-  sbi_embed_bi_embed :> BiEmbedding PROP1 PROP2;
-  sbi_embed_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y;
-  sbi_embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤
-}.
+Section embed_laws.
+  Context `{BiEmbed PROP1 PROP2}.
+  Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
+  Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
+  Implicit Types P : PROP1.
+
+  Global Instance embed_ne : NonExpansive embed.
+  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_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⎤.
+  Proof. eapply bi_embed_mixin_forall_2, bi_embed_mixin. Qed.
+  Lemma embed_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤.
+  Proof. eapply bi_embed_mixin_exist_1, bi_embed_mixin. Qed.
+  Lemma embed_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤.
+  Proof. eapply bi_embed_mixin_sep, bi_embed_mixin. Qed.
+  Lemma embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤.
+  Proof. eapply bi_embed_mixin_wand_2, bi_embed_mixin. Qed.
+  Lemma embed_plainly P : ⎡bi_plainly P⎤ ⊣⊢ bi_plainly ⎡P⎤.
+  Proof. eapply bi_embed_mixin_plainly, bi_embed_mixin. Qed.
+  Lemma embed_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤.
+  Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed.
+End embed_laws.
 
-Section bi_embedding.
-  Context `{BiEmbedding PROP1 PROP2}.
-  Local Notation bi_embed := (bi_embed (A:=PROP1) (B:=PROP2)).
-  Local Notation "⎡ P ⎤" := (bi_embed P) : bi_scope.
+Section embed.
+  Context `{BiEmbed PROP1 PROP2}.
+  Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
+  Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
   Implicit Types P Q R : PROP1.
 
-  Global Instance bi_embed_proper : Proper ((≡) ==> (≡)) bi_embed.
+  Global Instance embed_proper : Proper ((≡) ==> (≡)) embed.
   Proof. apply (ne_proper _). Qed.
-  Global Instance bi_embed_flip_mono : Proper (flip (⊢) ==> flip (⊢)) bi_embed.
+  Global Instance embed_flip_mono : Proper (flip (⊢) ==> flip (⊢)) embed.
   Proof. solve_proper. Qed.
-  Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed.
+  Global Instance embed_inj : Inj (≡) (≡) embed.
   Proof.
-    intros P Q EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
+    intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed);
     rewrite EQ //.
   Qed.
 
-  Lemma bi_embed_valid (P : PROP1) : ⎡P⎤%I ↔ P.
+  Lemma embed_valid (P : PROP1) : ⎡P⎤%I ↔ P.
   Proof.
-    by rewrite /bi_valid -bi_embed_emp; split=>?; [apply (inj bi_embed)|f_equiv].
+    by rewrite /bi_valid -embed_emp; split=>?; [apply (inj embed)|f_equiv].
   Qed.
 
-  Lemma bi_embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
+  Lemma embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
   Proof.
-    apply bi.equiv_spec; split; [|apply bi_embed_forall_2].
+    apply bi.equiv_spec; split; [|apply embed_forall_2].
     apply bi.forall_intro=>?. by rewrite bi.forall_elim.
   Qed.
-  Lemma bi_embed_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤.
+  Lemma embed_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤.
   Proof.
-    apply bi.equiv_spec; split; [apply bi_embed_exist_1|].
+    apply bi.equiv_spec; split; [apply embed_exist_1|].
     apply bi.exist_elim=>?. by rewrite -bi.exist_intro.
   Qed.
-  Lemma bi_embed_and P Q : ⎡P ∧ Q⎤ ⊣⊢ ⎡P⎤ ∧ ⎡Q⎤.
-  Proof. rewrite !bi.and_alt bi_embed_forall. by f_equiv=>-[]. Qed.
-  Lemma bi_embed_or P Q : ⎡P ∨ Q⎤ ⊣⊢ ⎡P⎤ ∨ ⎡Q⎤.
-  Proof. rewrite !bi.or_alt bi_embed_exist. by f_equiv=>-[]. Qed.
-  Lemma bi_embed_impl P Q : ⎡P → Q⎤ ⊣⊢ (⎡P⎤ → ⎡Q⎤).
+  Lemma embed_and P Q : ⎡P ∧ Q⎤ ⊣⊢ ⎡P⎤ ∧ ⎡Q⎤.
+  Proof. rewrite !bi.and_alt embed_forall. by f_equiv=>-[]. Qed.
+  Lemma embed_or P Q : ⎡P ∨ Q⎤ ⊣⊢ ⎡P⎤ ∨ ⎡Q⎤.
+  Proof. rewrite !bi.or_alt embed_exist. by f_equiv=>-[]. Qed.
+  Lemma embed_impl P Q : ⎡P → Q⎤ ⊣⊢ (⎡P⎤ → ⎡Q⎤).
   Proof.
-    apply bi.equiv_spec; split; [|apply bi_embed_impl_2].
-    apply bi.impl_intro_l. by rewrite -bi_embed_and bi.impl_elim_r.
+    apply bi.equiv_spec; split; [|apply embed_impl_2].
+    apply bi.impl_intro_l. by rewrite -embed_and bi.impl_elim_r.
   Qed.
-  Lemma bi_embed_wand P Q : ⎡P -∗ Q⎤ ⊣⊢ (⎡P⎤ -∗ ⎡Q⎤).
+  Lemma embed_wand P Q : ⎡P -∗ Q⎤ ⊣⊢ (⎡P⎤ -∗ ⎡Q⎤).
   Proof.
-    apply bi.equiv_spec; split; [|apply bi_embed_wand_2].
-    apply bi.wand_intro_l. by rewrite -bi_embed_sep bi.wand_elim_r.
+    apply bi.equiv_spec; split; [|apply embed_wand_2].
+    apply bi.wand_intro_l. by rewrite -embed_sep bi.wand_elim_r.
   Qed.
-  Lemma bi_embed_pure φ : ⎡⌜φ⌝⎤ ⊣⊢ ⌜φ⌝.
+  Lemma embed_pure φ : ⎡⌜φ⌝⎤ ⊣⊢ ⌜φ⌝.
   Proof.
-    rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_embed_exist.
+    rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) embed_exist.
     do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
-    rewrite -(_ : (emp → emp : PROP1) ⊢ True) ?bi_embed_impl;
+    rewrite -(_ : (emp → emp : PROP1) ⊢ True) ?embed_impl;
       last apply bi.True_intro.
     apply bi.impl_intro_l. by rewrite right_id.
   Qed.
-  Lemma bi_embed_iff P Q : ⎡P ↔ Q⎤ ⊣⊢ (⎡P⎤ ↔ ⎡Q⎤).
-  Proof. by rewrite bi_embed_and !bi_embed_impl. Qed.
-  Lemma bi_embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤).
-  Proof. by rewrite bi_embed_and !bi_embed_wand. Qed.
-  Lemma bi_embed_affinely P : ⎡bi_affinely P⎤ ⊣⊢ bi_affinely ⎡P⎤.
-  Proof. by rewrite bi_embed_and bi_embed_emp. Qed.
-  Lemma bi_embed_absorbingly P : ⎡bi_absorbingly P⎤ ⊣⊢ bi_absorbingly ⎡P⎤.
-  Proof. by rewrite bi_embed_sep bi_embed_pure. Qed.
-  Lemma bi_embed_plainly_if P b : ⎡bi_plainly_if b P⎤ ⊣⊢ bi_plainly_if b ⎡P⎤.
-  Proof. destruct b; simpl; auto using bi_embed_plainly. Qed.
-  Lemma bi_embed_persistently_if P b :
+  Lemma embed_iff P Q : ⎡P ↔ Q⎤ ⊣⊢ (⎡P⎤ ↔ ⎡Q⎤).
+  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 : ⎡bi_affinely P⎤ ⊣⊢ bi_affinely ⎡P⎤.
+  Proof. by rewrite embed_and embed_emp. Qed.
+  Lemma embed_absorbingly P : ⎡bi_absorbingly P⎤ ⊣⊢ bi_absorbingly ⎡P⎤.
+  Proof. by rewrite embed_sep embed_pure. Qed.
+  Lemma embed_plainly_if P b : ⎡bi_plainly_if b P⎤ ⊣⊢ bi_plainly_if b ⎡P⎤.
+  Proof. destruct b; simpl; auto using embed_plainly. Qed.
+  Lemma embed_persistently_if P b :
     ⎡bi_persistently_if b P⎤ ⊣⊢ bi_persistently_if b ⎡P⎤.
-  Proof. destruct b; simpl; auto using bi_embed_persistently. Qed.
-  Lemma bi_embed_affinely_if P b : ⎡bi_affinely_if b P⎤ ⊣⊢ bi_affinely_if b ⎡P⎤.
-  Proof. destruct b; simpl; auto using bi_embed_affinely. Qed.
-  Lemma bi_embed_hforall {As} (Φ : himpl As PROP1):
-    ⎡bi_hforall Φ⎤ ⊣⊢ bi_hforall (hcompose bi_embed Φ).
-  Proof. induction As=>//. rewrite /= bi_embed_forall. by do 2 f_equiv. Qed.
-  Lemma bi_embed_hexist {As} (Φ : himpl As PROP1):
-    ⎡bi_hexist Φ⎤ ⊣⊢ bi_hexist (hcompose bi_embed Φ).
-  Proof. induction As=>//. rewrite /= bi_embed_exist. by do 2 f_equiv. Qed.
-
-  Global Instance bi_embed_plain P : Plain P → Plain ⎡P⎤.
-  Proof. intros ?. by rewrite /Plain -bi_embed_plainly -plain. Qed.
-  Global Instance bi_embed_persistent P : Persistent P → Persistent ⎡P⎤.
-  Proof. intros ?. by rewrite /Persistent -bi_embed_persistently -persistent. Qed.
-  Global Instance bi_embed_affine P : Affine P → Affine ⎡P⎤.
-  Proof. intros ?. by rewrite /Affine (affine P) bi_embed_emp. Qed.
-  Global Instance bi_embed_absorbing P : Absorbing P → Absorbing ⎡P⎤.
-  Proof. intros ?. by rewrite /Absorbing -bi_embed_absorbingly absorbing. Qed.
-
-  Global Instance bi_embed_and_homomorphism :
-    MonoidHomomorphism bi_and bi_and (≡) bi_embed.
+  Proof. destruct b; simpl; auto using embed_persistently. Qed.
+  Lemma embed_affinely_if P b : ⎡bi_affinely_if b P⎤ ⊣⊢ bi_affinely_if b ⎡P⎤.
+  Proof. destruct b; simpl; auto using embed_affinely. 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.
+  Lemma embed_hexist {As} (Φ : himpl As PROP1):
+    ⎡bi_hexist Φ⎤ ⊣⊢ bi_hexist (hcompose embed Φ).
+  Proof. induction As=>//. rewrite /= embed_exist. by do 2 f_equiv. Qed.
+
+  Global Instance embed_plain P : Plain P → Plain ⎡P⎤.
+  Proof. intros ?. by rewrite /Plain -embed_plainly -plain. Qed.
+  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⎤.
+  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.
+
+  Global Instance embed_and_homomorphism :
+    MonoidHomomorphism bi_and bi_and (≡) embed.
   Proof.
     by split; [split|]; try apply _;
-      [setoid_rewrite bi_embed_and|rewrite bi_embed_pure].
+      [setoid_rewrite embed_and|rewrite embed_pure].
   Qed.
-  Global Instance bi_embed_or_homomorphism :
-    MonoidHomomorphism bi_or bi_or (≡) bi_embed.
+  Global Instance embed_or_homomorphism :
+    MonoidHomomorphism bi_or bi_or (≡) embed.
   Proof.
     by split; [split|]; try apply _;
-      [setoid_rewrite bi_embed_or|rewrite bi_embed_pure].
+      [setoid_rewrite embed_or|rewrite embed_pure].
   Qed.
-  Global Instance bi_embed_sep_homomorphism :
-    MonoidHomomorphism bi_sep bi_sep (≡) bi_embed.
+  Global Instance embed_sep_homomorphism :
+    MonoidHomomorphism bi_sep bi_sep (≡) embed.
   Proof.
     by split; [split|]; try apply _;
-      [setoid_rewrite bi_embed_sep|rewrite bi_embed_emp].
+      [setoid_rewrite embed_sep|rewrite embed_emp].
   Qed.
 
-  Lemma bi_embed_big_sepL {A} (Φ : nat → A → PROP1) l :
+  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 bi_embed_big_sepM `{Countable K} {A} (Φ : K → A → PROP1) (m : gmap K A) :
+  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 bi_embed_big_sepS `{Countable A} (Φ : A → PROP1) (X : gset A) :
+  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 bi_embed_big_sepMS `{Countable A} (Φ : A → PROP1) (X : gmultiset A) :
+  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 bi_embedding.
+End embed.
 
-Section sbi_embedding.
-  Context `{SbiEmbedding PROP1 PROP2}.
+Section sbi_embed.
+  Context `{SbiEmbed PROP1 PROP2}.
   Implicit Types P Q R : PROP1.
 
-  Lemma sbi_embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y.
+  Lemma embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y.
   Proof.
-    apply bi.equiv_spec; split; [apply sbi_embed_internal_eq_1|].
+    apply bi.equiv_spec; split; [apply embed_internal_eq_1|].
     etrans; [apply (bi.internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|].
-    rewrite -(bi.internal_eq_refl True%I) bi_embed_pure.
+    rewrite -(bi.internal_eq_refl True%I) embed_pure.
     eapply bi.impl_elim; [done|]. apply bi.True_intro.
   Qed.
-  Lemma sbi_embed_laterN n P : ⎡▷^n P⎤ ⊣⊢ ▷^n ⎡P⎤.
-  Proof. induction n=>//=. rewrite sbi_embed_later. by f_equiv. Qed.
-  Lemma sbi_embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
-  Proof. by rewrite bi_embed_or sbi_embed_later bi_embed_pure. Qed.
+  Lemma embed_laterN n P : ⎡▷^n P⎤ ⊣⊢ ▷^n ⎡P⎤.
+  Proof. induction n=>//=. rewrite embed_later. by f_equiv. Qed.
+  Lemma embed_except_0 P : ⎡◇ P⎤ ⊣⊢ ◇ ⎡P⎤.
+  Proof. by rewrite embed_or embed_later embed_pure. Qed.
 
-  Global Instance sbi_embed_timeless P : Timeless P → Timeless ⎡P⎤.
+  Global Instance embed_timeless P : Timeless P → Timeless ⎡P⎤.
   Proof.
-    intros ?. by rewrite /Timeless -sbi_embed_except_0 -sbi_embed_later timeless.
+    intros ?. by rewrite /Timeless -embed_except_0 -embed_later timeless.
   Qed.
-End sbi_embedding.
+End sbi_embed.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index aea516612d3538b7f06ad407ac76592bafe67091..3e37b6d53609fd6e5c20863818898804a8a7347a 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -2,7 +2,6 @@ From stdpp Require Import coPset.
 From iris.bi Require Import bi.
 
 (** Definitions. *)
-
 Structure biIndex :=
   BiIndex
     { bi_index_type :> Type;
@@ -128,14 +127,33 @@ Next Obligation. solve_proper. Qed.
 
 Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _.
 Definition monPred_embed_aux : seal (@monPred_embed_def). by eexists. Qed.
-Global Instance monPred_embed : BiEmbed PROP monPred := unseal monPred_embed_aux.
-Definition monPred_embed_eq : bi_embed (A:=PROP) = _ := seal_eq _.
-
-Definition monPred_pure (φ : Prop) : monPred := tc_opaque ⎡⌜φ⌝⎤%I.
-Definition monPred_emp : monPred := tc_opaque ⎡emp⎤%I.
-Definition monPred_plainly P : monPred := tc_opaque ⎡∀ i, bi_plainly (P i)⎤%I.
-Definition monPred_absolutely (P : monPred) : monPred := tc_opaque ⎡∀ i, P i⎤%I.
-Definition monPred_relatively (P : monPred) : monPred := tc_opaque ⎡∃ i, P i⎤%I.
+Definition monPred_embed : Embed PROP monPred := unseal monPred_embed_aux.
+Definition monPred_embed_eq : @embed _ _ monPred_embed = _ := seal_eq _.
+
+Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
+Definition monPred_emp_aux : seal (@monPred_emp_def). by eexists. Qed.
+Definition monPred_emp := unseal monPred_emp_aux.
+Definition monPred_emp_eq : @monPred_emp = _ := seal_eq _.
+
+Definition monPred_pure_def (φ : Prop) : monPred := MonPred (λ _, ⌜φ⌝)%I _.
+Definition monPred_pure_aux : seal (@monPred_pure_def). by eexists. Qed.
+Definition monPred_pure := unseal monPred_pure_aux.
+Definition monPred_pure_eq : @monPred_pure = _ := seal_eq _.
+
+Definition monPred_plainly_def P : monPred := MonPred (λ _, ∀ i, bi_plainly (P i))%I _.
+Definition monPred_plainly_aux : seal (@monPred_plainly_def). by eexists. Qed.
+Definition monPred_plainly := unseal monPred_plainly_aux.
+Definition monPred_plainly_eq : @monPred_plainly = _ := seal_eq _.
+
+Definition monPred_absolutely_def P : monPred := MonPred (λ _, ∀ i, P i)%I _.
+Definition monPred_absolutely_aux : seal (@monPred_absolutely_def). by eexists. Qed.
+Definition monPred_absolutely := unseal monPred_absolutely_aux.
+Definition monPred_absolutely_eq : @monPred_absolutely = _ := seal_eq _.
+
+Definition monPred_relatively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _.
+Definition monPred_relatively_aux : seal (@monPred_relatively_def). by eexists. Qed.
+Definition monPred_relatively := unseal monPred_relatively_aux.
+Definition monPred_relatively_eq : @monPred_relatively = _ := seal_eq _.
 
 Program Definition monPred_and_def P Q : monPred :=
   MonPred (λ i, P i ∧ Q i)%I _.
@@ -214,15 +232,16 @@ Arguments monPred_relatively {_ _} _%I.
 Notation "'∀ᵢ' P" := (monPred_absolutely P) (at level 20, right associativity) : bi_scope.
 Notation "'∃ᵢ' P" := (monPred_relatively P) (at level 20, right associativity) : bi_scope.
 
-Typeclasses Opaque monPred_pure monPred_emp monPred_plainly.
-
 Section Sbi.
 Context {I : biIndex} {PROP : sbi}.
 Implicit Types i : I.
 Notation monPred := (monPred I PROP).
 Implicit Types P Q : monPred.
 
-Definition monPred_internal_eq (A : ofeT) (a b : A) : monPred := tc_opaque ⎡a ≡ b⎤%I.
+Definition monPred_internal_eq_def (A : ofeT) (a b : A) : monPred := MonPred (λ _, a ≡ b)%I _.
+Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). by eexists. Qed.
+Definition monPred_internal_eq := unseal monPred_internal_eq_aux.
+Definition monPred_internal_eq_eq : @monPred_internal_eq = _ := seal_eq _.
 
 Program Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
 Next Obligation. solve_proper. Qed.
@@ -246,18 +265,18 @@ Definition unseal_eqs :=
   (@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq,
    @monPred_forall_eq, @monPred_exist_eq,
    @monPred_sep_eq, @monPred_wand_eq,
-   @monPred_persistently_eq, @monPred_later_eq, @monPred_in_eq,
-   @monPred_embed_eq, @monPred_bupd_eq, @monPred_fupd_eq).
+   @monPred_persistently_eq, @monPred_later_eq, @monPred_internal_eq_eq, @monPred_in_eq,
+   @monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq, @monPred_plainly_eq,
+   @monPred_absolutely_eq, @monPred_relatively_eq, @monPred_bupd_eq, @monPred_fupd_eq).
 Ltac unseal :=
   unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
-         monPred_absolutely, monPred_relatively, monPred_upclosed, bi_and, bi_or,
+         monPred_upclosed, bi_and, bi_or,
          bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand,
          bi_persistently, bi_affinely, bi_plainly, sbi_later;
   simpl;
   unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
          sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently, sbi_plainly;
   simpl;
-  unfold monPred_pure, monPred_emp, monPred_internal_eq, monPred_plainly; simpl;
   rewrite !unseal_eqs /=.
 End MonPred.
 Import MonPred.
@@ -322,7 +341,7 @@ Proof.
     repeat setoid_rewrite <-bi.plainly_forall.
     setoid_rewrite bi.plainly_impl_plainly. f_equiv.
     do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
-  - intros P. split=> i. apply bi.forall_intro=>_. by apply bi.plainly_emp_intro.
+  - intros P. split=> i /=. apply bi.forall_intro=>_. by apply bi.plainly_emp_intro.
   - intros P Q. split=> i. apply bi.sep_elim_l, _.
   - intros P Q [?]. split=> i /=. by f_equiv.
   - intros P. split=> i. by apply bi.persistently_idemp_2.
@@ -457,8 +476,7 @@ Global Instance monPred_in_absorbing i :
   Absorbing (@monPred_in I PROP i).
 Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed.
 
-
-Global Instance monPred_bi_embedding : BiEmbedding PROP monPredI.
+Definition monPred_embedding_mixin : BiEmbedMixin PROP monPredI monPred_embed.
 Proof.
   split; try apply _; unseal; try done.
   - move =>?? /= [/(_ inhabitant) ?] //.
@@ -469,61 +487,71 @@ Proof.
   - intros ?. split => ? /=. apply bi.equiv_spec; split.
     by apply bi.forall_intro. by rewrite bi.forall_elim.
 Qed.
+Global Instance monPred_bi_embed : BiEmbed PROP monPredI :=
+  {| bi_embed_mixin := monPred_embedding_mixin |}.
+
+Lemma monPred_emp_unfold : emp%I = ⎡emp : PROP⎤%I.
+Proof. by unseal. Qed.
+Lemma monPred_pure_unfold : bi_pure = λ φ, ⎡ ⌜ φ ⌝ : PROP⎤%I.
+Proof. by unseal. Qed.
+Lemma monPred_plainly_unfold : bi_plainly = λ P, ⎡ ∀ i, bi_plainly (P i) ⎤%I.
+Proof. by unseal. Qed.
+Lemma monPred_absolutely_unfold : monPred_absolutely = λ P, ⎡∀ i, P i⎤%I.
+Proof. by unseal. Qed.
+Lemma monPred_relatively_unfold : monPred_relatively = λ P, ⎡∃ i, P i⎤%I.
+Proof. by unseal. Qed.
 
 Global Instance monPred_absolutely_ne : NonExpansive (@monPred_absolutely I PROP).
-Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
+Proof. rewrite monPred_absolutely_unfold. solve_proper. Qed.
 Global Instance monPred_absolutely_proper : Proper ((≡) ==> (≡)) (@monPred_absolutely I PROP).
 Proof. apply (ne_proper _). Qed.
 Lemma monPred_absolutely_mono P Q : (P ⊢ Q) → (∀ᵢ P ⊢ ∀ᵢ Q).
-Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
+Proof. rewrite monPred_absolutely_unfold. solve_proper. Qed.
 Global Instance monPred_absolutely_mono' : Proper ((⊢) ==> (⊢)) (@monPred_absolutely I PROP).
-Proof. rewrite /monPred_absolutely /=. solve_proper. Qed.
+Proof. intros ???. by apply monPred_absolutely_mono. Qed.
 Global Instance monPred_absolutely_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@monPred_absolutely I PROP).
-Proof. solve_proper. Qed.
-
-Local Notation "'∀ᵢ' P" := (@monPred_absolutely I PROP P) : bi_scope.
-Local Notation "'∃ᵢ' P" := (@monPred_relatively I PROP P) : bi_scope.
+Proof. intros ???. by apply monPred_absolutely_mono. Qed.
 
 Global Instance monPred_absolutely_plain P : Plain P → Plain (∀ᵢ P).
-Proof. rewrite /monPred_absolutely /=. apply _. Qed.
+Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
 Global Instance monPred_absolutely_persistent P : Persistent P → Persistent (∀ᵢ P).
-Proof. rewrite /monPred_absolutely /=. apply _. Qed.
+Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
 Global Instance monPred_absolutely_absorbing P : Absorbing P → Absorbing (∀ᵢ P).
-Proof. rewrite /monPred_absolutely /=. apply _. Qed.
+Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
 Global Instance monPred_absolutely_affine P : Affine P → Affine (∀ᵢ P).
-Proof. rewrite /monPred_absolutely /=. apply _. Qed.
+Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
 
 Global Instance monPred_relatively_ne : NonExpansive (@monPred_relatively I PROP).
-Proof. rewrite /monPred_relatively /=. solve_proper. Qed.
+Proof. rewrite monPred_relatively_unfold. solve_proper. Qed.
 Global Instance monPred_relatively_proper : Proper ((≡) ==> (≡)) (@monPred_relatively I PROP).
 Proof. apply (ne_proper _). Qed.
 Lemma monPred_relatively_mono P Q : (P ⊢ Q) → (∃ᵢ P ⊢ ∃ᵢ Q).
-Proof. rewrite /monPred_relatively /=. solve_proper. Qed.
+Proof. rewrite monPred_relatively_unfold. solve_proper. Qed.
 Global Instance monPred_relatively_mono' : Proper ((⊢) ==> (⊢)) (@monPred_relatively I PROP).
-Proof. rewrite /monPred_relatively /=. solve_proper. Qed.
+Proof. intros ???. by apply monPred_relatively_mono. Qed.
 Global Instance monPred_relatively_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@monPred_relatively I PROP).
-Proof. solve_proper. Qed.
+Proof. intros ???. by apply monPred_relatively_mono. Qed.
 
 Global Instance monPred_relatively_plain P : Plain P → Plain (∃ᵢ P).
-Proof. rewrite /monPred_relatively /=. apply _. Qed.
+Proof. rewrite monPred_relatively_unfold. apply _. Qed.
 Global Instance monPred_relatively_persistent P : Persistent P → Persistent (∃ᵢ P).
-Proof. rewrite /monPred_relatively /=. apply _. Qed.
+Proof. rewrite monPred_relatively_unfold. apply _. Qed.
 Global Instance monPred_relatively_absorbing P : Absorbing P → Absorbing (∃ᵢ P).
-Proof. rewrite /monPred_relatively /=. apply _. Qed.
+Proof. rewrite monPred_relatively_unfold. apply _. Qed.
 Global Instance monPred_relatively_affine P : Affine P → Affine (∃ᵢ P).
-Proof. rewrite /monPred_relatively /=. apply _. Qed.
+Proof. rewrite monPred_relatively_unfold. apply _. Qed.
 
 (** monPred_at unfolding laws *)
 Lemma monPred_at_embed i (P : PROP) : monPred_at ⎡P⎤ i ⊣⊢ P.
 Proof. by unseal. Qed.
 Lemma monPred_at_pure i (φ : Prop) : monPred_at ⌜φ⌝ i ⊣⊢ ⌜φ⌝.
-Proof. by apply monPred_at_embed. Qed.
+Proof. by unseal. Qed.
 Lemma monPred_at_emp i : monPred_at emp i ⊣⊢ emp.
-Proof. by apply monPred_at_embed. Qed.
+Proof. by unseal. Qed.
 Lemma monPred_at_plainly i P : bi_plainly P i ⊣⊢ ∀ j, bi_plainly (P j).
-Proof. by apply monPred_at_embed. Qed.
+Proof. by unseal. Qed.
 Lemma monPred_at_and i P Q : (P ∧ Q) i ⊣⊢ P i ∧ Q i.
 Proof. by unseal. Qed.
 Lemma monPred_at_or i P Q : (P ∨ Q) i ⊣⊢ P i ∨ Q i.
@@ -544,7 +572,7 @@ Lemma monPred_at_in i j : monPred_at (monPred_in j) i ⊣⊢ ⌜j ⊑ i⌝.
 Proof. by unseal. Qed.
 Lemma monPred_at_absolutely i P : (∀ᵢ P) i ⊣⊢ ∀ j, P j.
 Proof. by unseal. Qed.
-Lemma monPred_at_ex i P : (∃ᵢ P) i ⊣⊢ ∃ j, P j.
+Lemma monPred_at_relatively i P : (∃ᵢ P) i ⊣⊢ ∃ j, P j.
 Proof. by unseal. Qed.
 Lemma monPred_at_persistently_if i p P :
   bi_persistently_if p P i ⊣⊢ bi_persistently_if p (P i).
@@ -564,7 +592,7 @@ Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed
 
 (* Laws for monPred_absolutely and of Absolute. *)
 Lemma monPred_absolutely_elim P : ∀ᵢ P ⊢ P.
-Proof. unseal. split=>?. apply bi.forall_elim. Qed.
+Proof. rewrite monPred_absolutely_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
 Lemma monPred_absolutely_idemp P : ∀ᵢ (∀ᵢ P) ⊣⊢ ∀ᵢ P.
 Proof.
   apply bi.equiv_spec; split; [by apply monPred_absolutely_elim|].
@@ -600,6 +628,10 @@ Proof.
   apply bi.equiv_spec; split; unseal; split=>i /=.
   by rewrite (bi.forall_elim inhabitant). by apply bi.forall_intro.
 Qed.
+Lemma monPred_absolutely_emp : ∀ᵢ (emp : monPred) ⊣⊢ emp.
+Proof. rewrite monPred_emp_unfold. apply monPred_absolutely_embed. Qed.
+Lemma monPred_absolutely_pure φ : ∀ᵢ (⌜ φ ⌝ : monPred) ⊣⊢ ⌜ φ ⌝.
+Proof. rewrite monPred_pure_unfold. apply monPred_absolutely_embed. Qed.
 
 Lemma monPred_relatively_intro P : P ⊢ ∃ᵢ P.
 Proof. unseal. split=>?. apply bi.exist_intro. Qed.
@@ -632,27 +664,27 @@ Qed.
 
 Lemma absolute_absolutely P `{!Absolute P} : P ⊢ ∀ᵢ P.
 Proof.
-  rewrite /monPred_absolutely /= bi_embed_forall. apply bi.forall_intro=>?.
+  rewrite monPred_absolutely_unfold /= embed_forall. apply bi.forall_intro=>?.
   split=>?. unseal. apply absolute_at, _.
 Qed.
 Lemma absolute_relatively P `{!Absolute P} : ∃ᵢ P ⊢ P.
 Proof.
-  rewrite /monPred_relatively /= bi_embed_exist. apply bi.exist_elim=>?.
+  rewrite monPred_relatively_unfold /= embed_exist. apply bi.exist_elim=>?.
   split=>?. unseal. apply absolute_at, _.
 Qed.
 
-Global Instance emb_absolute (P : PROP) : @Absolute I PROP ⎡P⎤.
+Global Instance embed_absolute (P : PROP) : @Absolute I PROP ⎡P⎤.
 Proof. intros ??. by unseal. Qed.
 Global Instance pure_absolute φ : @Absolute I PROP ⌜φ⌝.
-Proof. apply emb_absolute. Qed.
+Proof. intros ??. by unseal. Qed.
 Global Instance emp_absolute : @Absolute I PROP emp.
-Proof. apply emb_absolute. Qed.
+Proof. intros ??. by unseal. Qed.
 Global Instance plainly_absolute P : Absolute (bi_plainly P).
-Proof. apply emb_absolute. Qed.
+Proof. intros ??. by unseal. Qed.
 Global Instance absolutely_absolute P : Absolute (∀ᵢ P).
-Proof. apply emb_absolute. Qed.
+Proof. intros ??. by unseal. Qed.
 Global Instance relatively_absolute P : Absolute (∃ᵢ P).
-Proof. apply emb_absolute. Qed.
+Proof. intros ??. by unseal. Qed.
 
 Global Instance and_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∧ Q).
 Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
@@ -740,19 +772,19 @@ Global Instance monPred_absolutely_monoid_and_homomorphism :
   MonoidHomomorphism bi_and bi_and (≡) (@monPred_absolutely I PROP).
 Proof.
   split; [split|]; try apply _. apply monPred_absolutely_and.
-  apply monPred_absolutely_embed.
+  apply monPred_absolutely_pure.
 Qed.
 Global Instance monPred_absolutely_monoid_sep_entails_homomorphism :
   MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@monPred_absolutely I PROP).
 Proof.
   split; [split|]; try apply _. apply monPred_absolutely_sep_2.
-    by rewrite monPred_absolutely_embed.
+  by rewrite monPred_absolutely_emp.
 Qed.
 Global Instance monPred_absolutely_monoid_sep_homomorphism `{BiIndexBottom bot} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@monPred_absolutely I PROP).
 Proof.
   split; [split|]; try apply _. apply monPred_absolutely_sep.
-    by rewrite monPred_absolutely_embed.
+  by rewrite monPred_absolutely_emp.
 Qed.
 
 Lemma monPred_absolutely_big_sepL_entails {A} (Φ : nat → A → monPred) l :
@@ -862,9 +894,12 @@ Proof.
   by apply timeless, bi.exist_timeless.
 Qed.
 
-Global Instance monPred_sbi_embedding : SbiEmbedding PROP monPredSI.
+Global Instance monPred_sbi_embed : SbiEmbed PROP monPredSI.
 Proof. split; try apply _; by unseal. Qed.
 
+Lemma monPred_internal_eq_unfold : @sbi_internal_eq monPredSI = λ A x y, ⎡ x ≡ y ⎤%I.
+Proof. by unseal. Qed.
+
 Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredSI monPred_fupd.
 Proof.
   split; unseal; unfold monPred_fupd_def, monPred_upclosed.
@@ -903,7 +938,7 @@ Qed.
 (** Unfolding lemmas *)
 Lemma monPred_at_internal_eq {A : ofeT} i (a b : A) :
   @monPred_at I PROP (a ≡ b) i ⊣⊢ a ≡ b.
-Proof. by apply monPred_at_embed. Qed.
+Proof. rewrite monPred_internal_eq_unfold. by apply monPred_at_embed. Qed.
 Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
 Proof. by unseal. Qed.
 Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index f4932f9ee8b9bea1d2dcc31c1f5d57e6518ade15..7527d0f7a67bdaadb63d84f987373d12a15616d6 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -117,9 +117,9 @@ Proof. rewrite /IntoPure=> ->. apply: plainly_elim. Qed.
 Global Instance into_pure_persistently P φ :
   IntoPure P φ → IntoPure (bi_persistently P) φ.
 Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
-Global Instance into_pure_embed `{BiEmbedding PROP PROP'} P φ :
+Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ :
   IntoPure P φ → IntoPure ⎡P⎤ φ.
-Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed.
+Proof. rewrite /IntoPure=> ->. by rewrite embed_pure. Qed.
 
 (* FromPure *)
 Global Instance from_pure_pure a φ : @FromPure PROP a ⌜φ⌝ φ.
@@ -192,9 +192,9 @@ Proof. rewrite /FromPure /= affine_affinely //. Qed.
 Global Instance from_pure_absorbingly P φ :
   FromPure true P φ → FromPure false (bi_absorbingly P) φ.
 Proof. rewrite /FromPure=> <- /=. apply persistent_absorbingly_affinely, _. Qed.
-Global Instance from_pure_embed `{BiEmbedding PROP PROP'} a P φ :
+Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
   FromPure a P φ → FromPure a ⎡P⎤ φ.
-Proof. rewrite /FromPure=> <-. by rewrite bi_embed_affinely_if bi_embed_pure. Qed.
+Proof. rewrite /FromPure=> <-. by rewrite embed_affinely_if embed_pure. Qed.
 
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
@@ -206,10 +206,10 @@ Qed.
 Global Instance into_persistent_affinely p P Q :
   IntoPersistent p P Q → IntoPersistent p (bi_affinely P) Q | 0.
 Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
-Global Instance into_persistent_embed `{BiEmbedding PROP PROP'} p P Q :
+Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
   IntoPersistent p P Q → IntoPersistent p ⎡P⎤ ⎡Q⎤ | 0.
 Proof.
-  rewrite /IntoPersistent -bi_embed_persistently -bi_embed_persistently_if=> -> //.
+  rewrite /IntoPersistent -embed_persistently -embed_persistently_if=> -> //.
 Qed.
 Global Instance into_persistent_here P : IntoPersistent true P P | 1.
 Proof. by rewrite /IntoPersistent. Qed.
@@ -248,38 +248,38 @@ Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
 
 (* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
 the embedding over the modality. *)
-Global Instance from_modal_embed `{BiEmbedding PROP PROP'} (P : PROP) :
-  FromModal (@modality_embed PROP PROP' _ _) ⎡P⎤ ⎡P⎤ P.
+Global Instance from_modal_embed `{BiEmbed PROP PROP'} (P : PROP) :
+  FromModal (@modality_embed PROP PROP' _) ⎡P⎤ ⎡P⎤ P.
 Proof. by rewrite /FromModal. Qed.
 
-Global Instance from_modal_id_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+Global Instance from_modal_id_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
   FromModal modality_id sel P Q →
   FromModal modality_id sel ⎡P⎤ ⎡Q⎤ | 100.
 Proof. by rewrite /FromModal /= =><-. Qed.
 
-Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+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 bi_embed_affinely. Qed.
-Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+Proof. rewrite /FromModal /= =><-. by rewrite embed_affinely. 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.
-Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_persistently. Qed.
-Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+Proof. rewrite /FromModal /= =><-. by rewrite embed_persistently. Qed.
+Global Instance from_modal_affinely_persistently_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
   FromModal modality_affinely_persistently sel P Q →
   FromModal modality_affinely_persistently sel ⎡P⎤ ⎡Q⎤ | 100.
 Proof.
-  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
+  rewrite /FromModal /= =><-. by rewrite embed_affinely embed_persistently.
 Qed.
-Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+Global Instance from_modal_plainly_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
   FromModal modality_plainly sel P Q →
   FromModal modality_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
-Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_plainly. Qed.
-Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
+Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
+Global Instance from_modal_affinely_plainly_embed `{BiEmbed PROP PROP'} `(sel : A) P Q :
   FromModal modality_affinely_plainly sel P Q →
   FromModal modality_affinely_plainly sel ⎡P⎤ ⎡Q⎤ | 100.
 Proof.
-  rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
+  rewrite /FromModal /= =><-. by rewrite embed_affinely embed_plainly.
 Qed.
 
 (* IntoWand *)
@@ -363,26 +363,26 @@ Proof. by rewrite /IntoWand /= persistently_idemp. Qed.
 Global Instance into_wand_persistently_false `{!BiAffine PROP} q R P Q :
   IntoWand false q R P Q → IntoWand false q (bi_persistently R) P Q.
 Proof. by rewrite /IntoWand persistently_elim. Qed.
-Global Instance into_wand_embed `{BiEmbedding PROP PROP'} p q R P Q :
+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 -!bi_embed_persistently_if -!bi_embed_affinely_if
-          -bi_embed_wand => -> //.
+  rewrite /IntoWand -!embed_persistently_if -!embed_affinely_if
+          -embed_wand => -> //.
 Qed.
 
 (* FromWand *)
 Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
 Proof. by rewrite /FromWand. Qed.
-Global Instance from_wand_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
+Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   FromWand P Q1 Q2 → FromWand ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromWand -bi_embed_wand => <-. Qed.
+Proof. by rewrite /FromWand -embed_wand => <-. Qed.
 
 (* FromImpl *)
 Global Instance from_impl_impl P1 P2 : FromImpl (P1 → P2) P1 P2.
 Proof. by rewrite /FromImpl. Qed.
-Global Instance from_impl_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
+Global Instance from_impl_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   FromImpl P Q1 Q2 → FromImpl ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromImpl -bi_embed_impl => <-. Qed.
+Proof. by rewrite /FromImpl -embed_impl => <-. Qed.
 
 (* FromAnd *)
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
@@ -424,9 +424,9 @@ Global Instance from_and_persistently_sep P Q1 Q2 :
   FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
 Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
 
-Global Instance from_and_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
+Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromAnd -bi_embed_and => <-. Qed.
+Proof. by rewrite /FromAnd -embed_and => <-. Qed.
 
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) x l :
   Persistent (Φ 0 x) →
@@ -464,9 +464,9 @@ Global Instance from_sep_persistently P Q1 Q2 :
   FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
 
-Global Instance from_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
+Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromSep -bi_embed_sep => <-. Qed.
+Proof. by rewrite /FromSep -embed_sep => <-. Qed.
 
 Global Instance from_sep_big_sepL_cons {A} (Φ : nat → A → PROP) x l :
   FromSep ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
@@ -529,11 +529,11 @@ Proof.
   - by rewrite -persistently_and !persistently_idemp.
   - intros ->. by rewrite persistently_and.
 Qed.
-Global Instance into_and_embed `{BiEmbedding PROP PROP'} p P Q1 Q2 :
+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 -bi_embed_and -!bi_embed_persistently_if
-          -!bi_embed_affinely_if=> -> //.
+  rewrite /IntoAnd -embed_and -!embed_persistently_if
+          -!embed_affinely_if=> -> //.
 Qed.
 
 (* IntoSep *)
@@ -567,9 +567,9 @@ Qed.
 Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
 
-Global Instance into_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
+Global Instance into_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. rewrite /IntoSep -bi_embed_sep=> -> //. Qed.
+Proof. rewrite /IntoSep -embed_sep=> -> //. Qed.
 
 Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2) | 0.
@@ -645,9 +645,9 @@ Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 →
   FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
-Global Instance from_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
+Global Instance from_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
+Proof. by rewrite /FromOr -embed_or => <-. Qed.
 
 (* IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
@@ -667,9 +667,9 @@ Global Instance into_or_persistently P Q1 Q2 :
   IntoOr P Q1 Q2 →
   IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
-Global Instance into_or_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
+Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
-Proof. by rewrite /IntoOr -bi_embed_or => <-. Qed.
+Proof. by rewrite /IntoOr -embed_or => <-. Qed.
 
 (* FromExist *)
 Global Instance from_exist_exist {A} (Φ : A → PROP): FromExist (∃ a, Φ a) Φ.
@@ -689,9 +689,9 @@ Proof. rewrite /FromExist=> <-. by rewrite -plainly_exist_2. Qed.
 Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
-Global Instance from_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) :
+Global Instance from_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /FromExist -bi_embed_exist => <-. Qed.
+Proof. by rewrite /FromExist -embed_exist => <-. Qed.
 
 (* IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
@@ -724,9 +724,9 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed.
 Global Instance into_exist_persistently {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
-Global Instance into_exist_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) :
+Global Instance into_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /IntoExist -bi_embed_exist => <-. Qed.
+Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
 
 (* IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
@@ -740,9 +740,9 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
 Global Instance into_forall_persistently {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
-Global Instance into_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) :
+Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /IntoForall -bi_embed_forall => <-. Qed.
+Proof. by rewrite /IntoForall -embed_forall => <-. Qed.
 
 (* FromForall *)
 Global Instance from_forall_forall {A} (Φ : A → PROP) :
@@ -780,9 +780,9 @@ Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
 Global Instance from_forall_persistently {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
-Global Instance from_forall_embed `{BiEmbedding PROP PROP'} {A} P (Φ : A → PROP) :
+Global Instance from_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall ⎡P⎤%I (λ a, ⎡Φ a⎤%I).
-Proof. by rewrite /FromForall -bi_embed_forall => <-. Qed.
+Proof. by rewrite /FromForall -embed_forall => <-. Qed.
 
 (* IntoInv *)
 Global Instance into_inv_embed {PROP' : bi} `{BiEmbed PROP PROP'} P N :
@@ -843,26 +843,26 @@ Proof.
   by rewrite affinely_persistently_if_elim sep_elim_l.
 Qed.
 
-Global Instance make_embed_pure `{BiEmbedding PROP PROP'} φ :
+Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
   KnownMakeEmbed ⌜φ⌝ ⌜φ⌝.
-Proof. apply bi_embed_pure. Qed.
-Global Instance make_embed_emp `{BiEmbedding PROP PROP'} :
+Proof. apply embed_pure. Qed.
+Global Instance make_embed_emp `{BiEmbed PROP PROP'} :
   KnownMakeEmbed emp emp.
-Proof. apply bi_embed_emp. Qed.
-Global Instance make_embed_default `{BiEmbedding PROP PROP'} P :
+Proof. apply embed_emp. Qed.
+Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
   MakeEmbed P ⎡P⎤ | 100.
 Proof. by rewrite /MakeEmbed. Qed.
 
-Global Instance frame_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') R :
+Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
   Frame p R P Q → MakeEmbed Q Q' → KnownFrame p ⎡R⎤ ⎡P⎤ Q'.
 Proof.
   rewrite /KnownFrame /Frame /MakeEmbed => <- <-.
-  rewrite bi_embed_sep bi_embed_affinely_if bi_embed_persistently_if => //.
+  rewrite embed_sep embed_affinely_if embed_persistently_if => //.
 Qed.
-Global Instance frame_pure_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') φ :
+Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
   Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' → KnownFrame p ⌜φ⌝ ⎡P⎤ Q'.
 Proof.
-  rewrite /KnownFrame /Frame /MakeEmbed -bi_embed_pure. apply (frame_embed p P Q).
+  rewrite /KnownFrame /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q).
 Qed.
 
 Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
@@ -1083,9 +1083,9 @@ Proof.
   - intros x. apply H1. revert H2. by rewrite (bi.forall_elim x).
 Qed.
 
-Global Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP) :
+Global Instance as_valid_embed `{BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
   AsValid0 φ P → AsValid φ ⎡P⎤.
-Proof. rewrite /AsValid0 /AsValid=> ->. rewrite bi_embed_valid //. Qed.
+Proof. rewrite /AsValid0 /AsValid=> ->. rewrite embed_valid //. Qed.
 End bi_instances.
 
 Section sbi_instances.
@@ -1381,9 +1381,9 @@ Global Instance is_except_0_except_0 P : IsExcept0 (â—‡ P).
 Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
 Global Instance is_except_0_later P : IsExcept0 (â–· P).
 Proof. by rewrite /IsExcept0 except_0_later. Qed.
-Global Instance is_except_0_embed `{SbiEmbedding PROP PROP'} P :
+Global Instance is_except_0_embed `{SbiEmbed PROP PROP'} P :
   IsExcept0 P → IsExcept0 ⎡P⎤.
-Proof. by rewrite /IsExcept0 -sbi_embed_except_0=>->. Qed.
+Proof. by rewrite /IsExcept0 -embed_except_0=>->. Qed.
 Global Instance is_except_0_bupd `{BiBUpd PROP} P : IsExcept0 P → IsExcept0 (|==> P).
 Proof.
   rewrite /IsExcept0=> HP.
@@ -1410,10 +1410,10 @@ Global Instance from_modal_fupd E P `{BiFUpd PROP} :
   FromModal modality_id (|={E}=> P) (|={E}=> P) P.
 Proof. by rewrite /FromModal /= -fupd_intro. Qed.
 
-Global Instance from_modal_later_embed `{SbiEmbedding PROP PROP'} `(sel : A) n P Q :
+Global Instance from_modal_later_embed `{SbiEmbed PROP PROP'} `(sel : A) n P Q :
   FromModal (modality_laterN n) sel P Q →
   FromModal (modality_laterN n) sel ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /FromModal /= =><-. by rewrite sbi_embed_laterN. Qed.
+Proof. rewrite /FromModal /= =><-. by rewrite embed_laterN. Qed.
 
 (* IntoInternalEq *)
 Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
@@ -1432,9 +1432,9 @@ Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (bi_persistently P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
 Global Instance into_internal_eq_embed
-       `{SbiEmbedding PROP PROP'} {A : ofeT} (x y : A) P :
+       `{SbiEmbed PROP PROP'} {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq ⎡P⎤ x y.
-Proof. rewrite /IntoInternalEq=> ->. by rewrite sbi_embed_internal_eq. Qed.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
 
 (* IntoExcept0 *)
 Global Instance into_except_0_except_0 P : IntoExcept0 (â—‡ P) P.
@@ -1456,9 +1456,9 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_plainly. Qed.
 Global Instance into_except_0_persistently P Q :
   IntoExcept0 P Q → IntoExcept0 (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
-Global Instance into_except_0_embed `{SbiEmbedding PROP PROP'} P Q :
+Global Instance into_except_0_embed `{SbiEmbed PROP PROP'} P Q :
   IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /IntoExcept0=> ->. by rewrite sbi_embed_except_0. Qed.
+Proof. rewrite /IntoExcept0=> ->. by rewrite embed_except_0. Qed.
 
 (* ElimModal *)
 Global Instance elim_modal_timeless P Q :
@@ -1517,10 +1517,10 @@ Global Instance add_modal_fupd `{BiFUpd PROP} E1 E2 P Q :
 Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 
 (* Frame *)
-Global Instance frame_eq_embed `{SbiEmbedding PROP PROP'} p P Q (Q' : PROP')
+Global Instance frame_eq_embed `{SbiEmbed PROP PROP'} p P Q (Q' : PROP')
        {A : ofeT} (a b : A) :
   Frame p (a ≡ b) P Q → MakeEmbed Q Q' → KnownFrame p (a ≡ b) ⎡P⎤ Q'.
-Proof. rewrite /KnownFrame /Frame /MakeEmbed -sbi_embed_internal_eq. apply (frame_embed p P Q). Qed.
+Proof. rewrite /KnownFrame /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
 
 Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
 Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
@@ -1635,9 +1635,9 @@ Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed
 Global Instance into_later_persistently n P Q :
   IntoLaterN false n P Q → IntoLaterN false n (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
-Global Instance into_later_embed`{SbiEmbedding PROP PROP'} n P Q :
+Global Instance into_later_embed`{SbiEmbed PROP PROP'} n P Q :
   IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤.
-Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed.
+Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite embed_laterN. Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
   IntoLaterN false n P1 Q1 → MaybeIntoLaterN false n P2 Q2 →
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
index 8fcfc827a9fa7e302292bc728f778235490eb5b9..197be17f0a52b575ac9c3738e4b83b27ea68db31 100644
--- a/theories/proofmode/modality_instances.v
+++ b/theories/proofmode/modality_instances.v
@@ -54,17 +54,17 @@ Section bi_modalities.
   Definition modality_affinely_plainly :=
     Modality _ modality_affinely_plainly_mixin.
 
-  Lemma modality_embed_mixin `{BiEmbedding PROP PROP'} :
-    modality_mixin (@bi_embed PROP PROP' _)
+  Lemma modality_embed_mixin `{BiEmbed PROP PROP'} :
+    modality_mixin (@embed PROP PROP' _)
       (MIEnvTransform IntoEmbed) (MIEnvTransform IntoEmbed).
   Proof.
     split; simpl; split_and?;
-      eauto using equiv_entails_sym, bi_embed_emp, bi_embed_sep, bi_embed_and.
+      eauto using equiv_entails_sym, embed_emp, embed_sep, embed_and.
     - intros P Q. rewrite /IntoEmbed=> ->.
-      by rewrite bi_embed_affinely bi_embed_persistently.
+      by rewrite embed_affinely embed_persistently.
     - by intros P Q ->.
   Qed.
-  Definition modality_embed `{BiEmbedding PROP PROP'} :=
+  Definition modality_embed `{BiEmbed PROP PROP'} :=
     Modality _ modality_embed_mixin.
 End bi_modalities.
 
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 2eb561cc2e8f8cbabb7d2027ea40a2261642e6d3..ecd669fd329ee71805af21da5b2d2f89f60f4601 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -319,12 +319,12 @@ Qed.
 Global Instance from_exist_monPred_at_ex P (Φ : I → PROP) i :
   (∀ i, MakeMonPredAt i P (Φ i)) → FromExist ((∃ᵢ P) i) Φ.
 Proof.
-  rewrite /FromExist /MakeMonPredAt monPred_at_ex=>H. by setoid_rewrite <- H.
+  rewrite /FromExist /MakeMonPredAt monPred_at_relatively=>H. by setoid_rewrite <- H.
 Qed.
 Global Instance into_exist_monPred_at_ex P (Φ : I → PROP) i :
   (∀ i, MakeMonPredAt i P (Φ i)) → IntoExist ((∃ᵢ P) i) Φ.
 Proof.
-  rewrite /IntoExist /MakeMonPredAt monPred_at_ex=>H. by setoid_rewrite <- H.
+  rewrite /IntoExist /MakeMonPredAt monPred_at_relatively=>H. by setoid_rewrite <- H.
 Qed.
 
 Global Instance from_forall_monPred_at {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
@@ -361,7 +361,10 @@ Qed.
 
 Global Instance into_embed_absolute P :
   Absolute P → IntoEmbed P (∀ i, P i).
-Proof. rewrite /IntoEmbed=> ?. by rewrite {1}(absolute_absolutely P). Qed.
+Proof.
+  rewrite /IntoEmbed=> ?.
+  by rewrite {1}(absolute_absolutely P) monPred_absolutely_unfold.
+Qed.
 
 Global Instance elim_modal_embed_bupd_goal `{BiBUpd PROP} φ P P' 𝓠 𝓠' :
   ElimModal φ P P' (|==> ⎡𝓠⎤)%I (|==> ⎡𝓠'⎤)%I →