From e39f72feb816b77f4aad0f689027f12668e9f1d4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Mar 2018 23:46:24 +0100
Subject: [PATCH] Bundle type class for embedding.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This change is slightly more invasive than expected: in monPred we were
using the embedding before the BI was defined. With the new setup, this
is no longer possible, because in order to make an instance of the
embedding, we need to know that `monPred` is a BI. As such, we define
`emp`, `⌜ _ ⌝` and friends directly in the model of `monPred` and later
prove that they are equal to a version in terms of the embedding.
---
 theories/bi/embedding.v                 | 250 ++++++++++++++----------
 theories/bi/monpred.v                   | 147 ++++++++------
 theories/proofmode/class_instances.v    | 140 ++++++-------
 theories/proofmode/modality_instances.v |  10 +-
 theories/proofmode/monpred.v            |   9 +-
 5 files changed, 314 insertions(+), 242 deletions(-)

diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 635d39dc3..957a827d9 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 aea516612..3e37b6d53 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 f4932f9ee..7527d0f7a 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 8fcfc827a..197be17f0 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 2eb561cc2..ecd669fd3 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 →
-- 
GitLab