diff --git a/_CoqProject b/_CoqProject
index da21ad5aff00407dcdd3c4d7f10257b7913b9cf0..6b739e43e9ec0775d9a4c3f88fe145a3a4c1fc84 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -36,6 +36,7 @@ theories/bi/fractional.v
 theories/bi/counter_examples.v
 theories/bi/fixpoint.v
 theories/bi/monpred.v
+theories/bi/embedding.v
 theories/base_logic/upred.v
 theories/base_logic/derived.v
 theories/base_logic/base_logic.v
@@ -91,10 +92,12 @@ theories/proofmode/tactics.v
 theories/proofmode/notation.v
 theories/proofmode/classes.v
 theories/proofmode/class_instances.v
+theories/proofmode/monpred.v
 theories/tests/heap_lang.v
 theories/tests/one_shot.v
 theories/tests/proofmode.v
 theories/tests/proofmode_iris.v
+theories/tests/proofmode_monpred.v
 theories/tests/list_reverse.v
 theories/tests/tree_sum.v
 theories/tests/ipm_paper.v
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index c0846ea376d94809ddf816012f093cf3b804fcba..4cef163c554776a75c9fd03b053716d240e90d0d 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export derived_laws big_op updates.
+From iris.bi Require Export derived_laws big_op updates embedding.
 Set Default Proof Using "Type".
 
 Module Import bi.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
new file mode 100644
index 0000000000000000000000000000000000000000..b42903ad94f6cfe31210790edbf689d190982382
--- /dev/null
+++ b/theories/bi/embedding.v
@@ -0,0 +1,161 @@
+From iris.algebra Require Import monoid.
+From iris.bi Require Import interface derived_laws.
+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.
+
+Hint Mode BiEmbed ! - : typeclass_instances.
+Hint Mode BiEmbed - ! : typeclass_instances.
+
+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_internal_eq_1 (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊢ x ≡ y;
+  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 SbiEmbedding (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
+  sbi_embed_bi_embed :> BiEmbedding PROP1 PROP2;
+  sbi_embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤
+}.
+
+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.
+  Implicit Types P Q R : PROP1.
+
+  Global Instance bi_embed_proper : Proper ((≡) ==> (≡)) bi_embed.
+  Proof. apply (ne_proper _). Qed.
+  Global Instance bi_embed_mono_flip : Proper (flip (⊢) ==> flip (⊢)) bi_embed.
+  Proof. solve_proper. Qed.
+  Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed.
+  Proof.
+    intros P Q EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
+    rewrite EQ //.
+  Qed.
+
+  Lemma bi_embed_valid (P : PROP1) : ⎡P⎤%I ↔ P.
+  Proof.
+    by rewrite /bi_valid -bi_embed_emp; split=>?; [apply (inj bi_embed)|f_equiv].
+  Qed.
+
+  Lemma bi_embed_forall A (Φ : A → PROP1) : ⎡∀ x, Φ x⎤ ⊣⊢ ∀ x, ⎡Φ x⎤.
+  Proof.
+    apply bi.equiv_spec; split; [|apply bi_embed_forall_2].
+    apply bi.forall_intro=>?. by rewrite bi.forall_elim.
+  Qed.
+  Lemma bi_embed_exist A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊣⊢ ∃ x, ⎡Φ x⎤.
+  Proof.
+    apply bi.equiv_spec; split; [apply bi_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⎤).
+  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.
+  Qed.
+  Lemma bi_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.
+  Qed.
+  Lemma bi_embed_pure φ : ⎡⌜φ⌝⎤ ⊣⊢ ⌜φ⌝.
+  Proof.
+    rewrite (@bi.pure_alt PROP1) (@bi.pure_alt PROP2) bi_embed_exist.
+    do 2 f_equiv. apply bi.equiv_spec. split; [apply bi.True_intro|].
+    rewrite -(_ : (emp → emp : PROP1) ⊢ True) ?bi_embed_impl;
+      last apply bi.True_intro.
+    apply bi.impl_intro_l. by rewrite right_id.
+  Qed.
+  Lemma bi_embed_internal_eq (A : ofeT) (x y : A) : ⎡x ≡ y⎤ ⊣⊢ x ≡ y.
+  Proof.
+    apply bi.equiv_spec; split; [apply bi_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.
+    eapply bi.impl_elim; [done|]. apply bi.True_intro.
+  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 :
+    ⎡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.
+    by split; [split|]; try apply _;
+      [setoid_rewrite bi_embed_and|rewrite bi_embed_pure].
+  Qed.
+  Global Instance bi_embed_or_homomorphism :
+    MonoidHomomorphism bi_or bi_or (≡) bi_embed.
+  Proof.
+    by split; [split|]; try apply _;
+      [setoid_rewrite bi_embed_or|rewrite bi_embed_pure].
+  Qed.
+  Global Instance bi_embed_sep_homomorphism :
+    MonoidHomomorphism bi_sep bi_sep (≡) bi_embed.
+  Proof.
+    by split; [split|]; try apply _;
+      [setoid_rewrite bi_embed_sep|rewrite bi_embed_emp].
+  Qed.
+End bi_embedding.
+
+Section sbi_embedding.
+  Context `{SbiEmbedding PROP1 PROP2}.
+  Implicit Types P Q R : PROP1.
+
+  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.
+
+  Global Instance sbi_embed_timeless P : Timeless P → Timeless ⎡P⎤.
+  Proof.
+    intros ?. by rewrite /Timeless -sbi_embed_except_0 -sbi_embed_later timeless.
+  Qed.
+End sbi_embedding.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 0105c21ebb5ef47633b435083e1d0f91e8801867..2add9f305138526a0f9517873b90a5cfc49973c9 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -329,14 +329,6 @@ Coercion sbi_valid {PROP : sbi} : PROP → Prop := bi_valid.
 Arguments bi_valid {_} _%I : simpl never.
 Typeclasses Opaque bi_valid.
 
-(* Typically, embeddings are used to *define* the destination BI.
-   Hence we cannot ask B to be a BI. *)
-Class BiEmbedding (A B : Type) := bi_embedding : A → B.
-Arguments bi_embedding {_ _ _} _%I : simpl never.
-Notation "⎡ P ⎤" := (bi_embedding P) : bi_scope.
-Instance: Params (@bi_embedding) 3.
-Typeclasses Opaque bi_embedding.
-
 Module bi.
 Section bi_laws.
 Context {PROP : bi}.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index b98c092bbf4e8e2aa7dc1d0f163852fd4c934ee3..0a355aa93aaec0d31c2b66862bd9e49e01041873 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -1,4 +1,4 @@
-From iris.bi Require Import derived_laws.
+From iris.bi Require Import bi.
 
 (** Definitions. *)
 
@@ -97,6 +97,7 @@ Proof. repeat intro. apply equiv_dist=>?. f_equiv=>//. by apply equiv_dist. Qed.
 End Ofe_Cofe.
 
 Arguments monPred _ _ : clear implicits.
+Arguments monPred_car {_ _} _%I _.
 Local Existing Instance monPred_mono.
 Arguments monPredC _ _ : clear implicits.
 
@@ -116,10 +117,10 @@ Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
   MonPred (λ i, (∀ j, ⌜i ⊑ j⌝ → Φ j)%I) _.
 Next Obligation. solve_proper. Qed.
 
-Definition monPred_ipure_def (P : PROP) : monPred := MonPred (λ _, P) _.
-Definition monPred_ipure_aux : seal (@monPred_ipure_def). by eexists. Qed.
-Global Instance monPred_ipure : BiEmbedding PROP monPred := unseal monPred_ipure_aux.
-Definition monPred_ipure_eq : bi_embedding = _ := seal_eq _.
+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 := ⎡⌜φ⌝⎤%I.
 Definition monPred_emp : monPred := ⎡emp⎤%I.
@@ -215,7 +216,7 @@ Definition unseal_eqs :=
    @monPred_forall_eq, @monPred_exist_eq, @monPred_internal_eq_eq,
    @monPred_sep_eq, @monPred_wand_eq,
    @monPred_persistently_eq, @monPred_later_eq,
-   @monPred_in_eq, @monPred_all_eq, @monPred_ipure_eq).
+   @monPred_in_eq, @monPred_all_eq, @monPred_embed_eq).
 Ltac unseal :=
   unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
          monPred_upclosed, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
@@ -372,19 +373,6 @@ Global Instance monPred_car_mono_flip :
   Proper (flip (⊢) ==> flip (⊑) ==> flip (⊢)) (@monPred_car I PROP).
 Proof. solve_proper. Qed.
 
-Global Instance monPred_ipure_ne :
-  NonExpansive (@bi_embedding PROP (monPred I PROP) _).
-Proof. unseal. by split. Qed.
-Global Instance monPred_ipure_proper :
-  Proper ((≡) ==> (≡)) (@bi_embedding PROP (monPred I PROP) _).
-Proof. apply (ne_proper _). Qed.
-Global Instance monPred_ipure_mono :
-  Proper ((⊢) ==> (⊢)) (@bi_embedding PROP (monPred I PROP) _).
-Proof. unseal. by split. Qed.
-Global Instance monPred_ipure_mono_flip :
-  Proper (flip (⊢) ==> flip (⊢)) (@bi_embedding PROP (monPred I PROP) _).
-Proof. solve_proper. Qed.
-
 Global Instance monPred_in_proper (R : relation I) :
   Proper (R ==> R ==> iff) (⊑) → Reflexive R →
   Proper (R ==> (≡)) (@monPred_in I PROP).
@@ -426,6 +414,10 @@ Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed
 Lemma monPred_impl_force P Q i : (P → Q) i -∗ (P i → Q i).
 Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
 
+Lemma monPred_car_embed (P : PROP) (i : I) :
+  (bi_embed (B := monPred _ _) P) i ⊣⊢ P.
+Proof. by unseal. Qed.
+
 Lemma monPred_persistently_if_eq p P i:
   (bi_persistently_if p P) i = bi_persistently_if p (P i).
 Proof. rewrite /bi_persistently_if. unseal. by destruct p. Qed.
@@ -443,19 +435,6 @@ Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed.
 Global Instance monPred_car_affine P i : Affine P → Affine (P i).
 Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
 
-Global Instance monPred_ipure_plain (P : PROP) :
-  Plain P → @Plain (monPredI I PROP) ⎡P⎤%I.
-Proof. split => ? /=. unseal. apply bi.forall_intro=>?. apply (plain _). Qed.
-Global Instance monPred_ipure_persistent (P : PROP) :
-  Persistent P → @Persistent (monPredI I PROP) ⎡P⎤%I.
-Proof. split => ? /=. unseal. exact: H. Qed.
-Global Instance monPred_ipure_absorbing (P : PROP) :
-  Absorbing P → @Absorbing (monPredI I PROP) ⎡P⎤%I.
-Proof. unfold Absorbing. split => ? /=. by unseal. Qed.
-Global Instance monPred_ipure_affine (P : PROP) :
-  Affine P → @Affine (monPredI I PROP) ⎡P⎤%I.
-Proof. unfold Affine. split => ? /=. by unseal. Qed.
-
 (* Note that monPred_in is *not* Plain, because it does depend on the
    index. *)
 Global Instance monPred_in_persistent V :
@@ -489,6 +468,18 @@ Proof.
   move=> []. unfold Affine. unseal=>Hp. split => ?.
   by apply affine, bi.forall_affine.
 Qed.
+
+Global Instance monPred_bi_embedding : BiEmbedding PROP (monPredI I PROP).
+Proof.
+  split; try apply _; unseal; try done.
+  - move =>?? /= [/(_ inhabitant) ?] //.
+  - split=>? /=.
+    by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
+  - split=>? /=.
+    by rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim.
+  - intros ?. split => ? /=. apply bi.equiv_spec; split.
+    by apply bi.forall_intro. by rewrite bi.forall_elim.
+Qed.
 End bi_facts.
 
 Section sbi_facts.
@@ -498,7 +489,7 @@ Implicit Types P Q : monPred I PROP.
 
 Global Instance monPred_car_timeless P i : Timeless P → Timeless (P i).
 Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
-Global Instance monPred_ipure_timeless (P : PROP) :
+Global Instance monPred_embed_timeless (P : PROP) :
   Timeless P → @Timeless (monPredSI I PROP) ⎡P⎤%I.
 Proof. intros. split => ? /=. by unseal. Qed.
 Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
@@ -509,4 +500,7 @@ Proof.
   move=>[]. unfold Timeless. unseal=>Hti. split=> ? /=.
   by apply timeless, bi.forall_timeless.
 Qed.
+
+Global Instance monPred_sbi_embedding : SbiEmbedding PROP (monPredSI I PROP).
+Proof. split; try apply _. by unseal. Qed.
 End sbi_facts.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index a75fe20cf9e1df233f8ff3639e91310a768845d9..d9e42bee2135f0eda69d694df9f6ed97db37fee6 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -115,6 +115,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 φ :
+  IntoPure P φ → IntoPure ⎡P⎤ φ.
+Proof. rewrite /IntoPure=> ->. by rewrite bi_embed_pure. Qed.
 
 (* FromPure *)
 Global Instance from_pure_pure φ : @FromPure PROP ⌜φ⌝ φ.
@@ -161,6 +164,9 @@ Global Instance from_pure_affinely P φ `{!Affine P} :
 Proof. by rewrite /FromPure affine_affinely. Qed.
 Global Instance from_pure_absorbingly P φ : FromPure P φ → FromPure (bi_absorbingly P) φ.
 Proof. rewrite /FromPure=> <-. by rewrite absorbingly_pure. Qed.
+Global Instance from_pure_embed `{BiEmbedding PROP PROP'} P φ :
+  FromPure P φ → FromPure ⎡P⎤ φ.
+Proof. rewrite /FromPure=> <-. by rewrite bi_embed_pure. Qed.
 
 (* IntoInternalEq *)
 Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
@@ -178,6 +184,10 @@ Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
 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
+       `{BiEmbedding PROP PROP'} {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq ⎡P⎤ x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite bi_embed_internal_eq. Qed.
 
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
@@ -189,6 +199,11 @@ 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 :
+  IntoPersistent p P Q → IntoPersistent p ⎡P⎤ ⎡Q⎤ | 0.
+Proof.
+  rewrite /IntoPersistent -bi_embed_persistently -bi_embed_persistently_if=> -> //.
+Qed.
 Global Instance into_persistent_here P : IntoPersistent true P P | 1.
 Proof. by rewrite /IntoPersistent. Qed.
 Global Instance into_persistent_persistent P :
@@ -216,6 +231,12 @@ Global Instance from_always_affinely a pe pl P Q :
 Proof.
   rewrite /FromAlways /= => <-. destruct a; by rewrite /= ?affinely_idemp.
 Qed.
+Global Instance from_always_embed `{BiEmbedding PROP PROP'} a pe pl P Q :
+  FromAlways a pe pl P Q → FromAlways a pe pl ⎡P⎤ ⎡Q⎤ | 0.
+Proof.
+  rewrite /FromAlways=><-.
+  by rewrite bi_embed_affinely_if bi_embed_persistently_if bi_embed_plainly_if.
+Qed.
 
 (* IntoWand *)
 Global Instance into_wand_wand p q P Q P' :
@@ -302,6 +323,12 @@ 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 :
+  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 => -> //.
+Qed.
 
 (* FromAnd *)
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2 | 100.
@@ -343,6 +370,10 @@ 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 :
+  FromAnd P Q1 Q2 → FromAnd ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromAnd -bi_embed_and => <-. Qed.
+
 Global Instance from_and_big_sepL_cons_persistent {A} (Φ : nat → A → PROP) x l :
   Persistent (Φ 0 x) →
   FromAnd ([∗ list] k ↦ y ∈ x :: l, Φ k y) (Φ 0 x) ([∗ list] k ↦ y ∈ l, Φ (S k) y).
@@ -379,6 +410,10 @@ 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 :
+  FromSep P Q1 Q2 → FromSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromSep -bi_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).
 Proof. by rewrite /FromSep big_sepL_cons. Qed.
@@ -436,6 +471,12 @@ 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 :
+  IntoAnd p P Q1 Q2 → IntoAnd p ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof.
+  rewrite /IntoAnd -bi_embed_and -!bi_embed_persistently_if
+          -!bi_embed_affinely_if=> -> //.
+Qed.
 
 (* IntoSep *)
 Global Instance into_sep_sep P Q : IntoSep (P ∗ Q) P Q.
@@ -469,6 +510,10 @@ 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 :
+  IntoSep P Q1 Q2 → IntoSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. rewrite /IntoSep -bi_embed_sep=> -> //. Qed.
+
 (* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely. Also, it
 overlaps with `into_sep_affinely_later`, and hence has lower precedence. *)
 Global Instance into_sep_affinely P Q1 Q2 :
@@ -515,6 +560,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 :
+  FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /FromOr -bi_embed_or => <-. Qed.
 
 (* IntoOr *)
 Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
@@ -534,6 +582,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 :
+  IntoOr P Q1 Q2 → IntoOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
+Proof. by rewrite /IntoOr -bi_embed_or => <-. Qed.
 
 (* FromExist *)
 Global Instance from_exist_exist {A} (Φ : A → PROP): FromExist (∃ a, Φ a) Φ.
@@ -553,6 +604,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) :
+  FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /FromExist -bi_embed_exist => <-. Qed.
 
 (* IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
@@ -585,6 +639,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) :
+  IntoExist P Φ → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /IntoExist -bi_embed_exist => <-. Qed.
 
 (* IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
@@ -598,6 +655,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) :
+  IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /IntoForall -bi_embed_forall => <-. Qed.
 
 (* FromForall *)
 Global Instance from_forall_forall {A} (Φ : A → PROP) :
@@ -635,6 +695,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) :
+  FromForall P Φ → FromForall ⎡P⎤%I (λ a, ⎡Φ a⎤%I).
+Proof. by rewrite /FromForall -bi_embed_forall => <-. Qed.
 
 (* ElimModal *)
 Global Instance elim_modal_wand P P' Q Q' R :
@@ -673,6 +736,26 @@ Proof.
   rewrite /FromPure /Frame=> <-. by rewrite affinely_persistently_if_elim sep_elim_l.
 Qed.
 
+Class MakeMorphism `{BiEmbedding PROP PROP'} P (Q : PROP') :=
+  make_embed : ⎡P⎤ ⊣⊢ Q.
+Arguments MakeMorphism {_ _ _} _%I _%I.
+Global Instance make_embed_pure `{BiEmbedding PROP PROP'} φ :
+  MakeMorphism ⌜φ⌝ ⌜φ⌝.
+Proof. by rewrite /MakeMorphism bi_embed_pure. Qed.
+Global Instance make_embed_emp `{BiEmbedding PROP PROP'} :
+  MakeMorphism emp emp.
+Proof. by rewrite /MakeMorphism bi_embed_emp. Qed.
+Global Instance make_embed_default `{BiEmbedding PROP PROP'} :
+  MakeMorphism P ⎡P⎤ | 100.
+Proof. by rewrite /MakeMorphism. Qed.
+
+Global Instance frame_embed `{BiEmbedding PROP PROP'} p P Q (Q' : PROP') R :
+  Frame p R P Q → MakeMorphism Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
+Proof.
+  rewrite /Frame /MakeMorphism => <- <-.
+  rewrite bi_embed_sep bi_embed_affinely_if bi_embed_persistently_if => //.
+Qed.
+
 Class MakeSep (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ.
 Arguments MakeSep _%I _%I _%I.
 Global Instance make_sep_emp_l P : MakeSep emp P P.
@@ -851,6 +934,9 @@ Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 (* FromModal *)
 Global Instance from_modal_absorbingly P : FromModal (bi_absorbingly P) P.
 Proof. apply absorbingly_intro. Qed.
+Global Instance from_modal_embed `{BiEmbedding PROP PROP'} P Q :
+  FromModal P Q → FromModal ⎡P⎤ ⎡Q⎤.
+Proof. by rewrite /FromModal=> ->. Qed.
 End bi_instances.
 
 
@@ -1057,6 +1143,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 :
+  IsExcept0 P → IsExcept0 ⎡P⎤.
+Proof. by rewrite /IsExcept0 -sbi_embed_except_0=>->. Qed.
 
 (* FromModal *)
 Global Instance from_modal_later P : FromModal (â–· P) P.
@@ -1084,6 +1173,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 :
+  IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /IntoExcept0=> ->. by rewrite sbi_embed_except_0. Qed.
 
 (* ElimModal *)
 Global Instance elim_modal_timeless P Q :
@@ -1190,6 +1282,9 @@ Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_plainly. Qed.
 Global Instance into_later_persistently n P Q :
   IntoLaterN n P Q → IntoLaterN n (bi_persistently P) (bi_persistently Q).
 Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
+Global Instance into_later_embed`{SbiEmbedding PROP PROP'} n P Q :
+  IntoLaterN n P Q → IntoLaterN n ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /IntoLaterN=> ->. by rewrite sbi_embed_laterN. Qed.
 
 Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
   IntoLaterN' n P1 Q1 → IntoLaterN n P2 Q2 →
@@ -1273,6 +1368,9 @@ Proof. by rewrite /FromLaterN laterN_persistently=> ->. Qed.
 Global Instance from_later_absorbingly n P Q :
   FromLaterN n P Q → FromLaterN n (bi_absorbingly P) (bi_absorbingly Q).
 Proof. by rewrite /FromLaterN laterN_absorbingly=> ->. Qed.
+Global Instance from_later_embed`{SbiEmbedding PROP PROP'} n P Q :
+  FromLaterN n P Q → FromLaterN n ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromLaterN=> <-. by rewrite sbi_embed_laterN. Qed.
 
 Global Instance from_later_forall {A} n (Φ Ψ : A → PROP) :
   (∀ x, FromLaterN n (Φ x) (Ψ x)) → FromLaterN n (∀ x, Φ x) (∀ x, Ψ x).
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
new file mode 100644
index 0000000000000000000000000000000000000000..a3afd86cccd638e56591cc6bf94e26c74decdd89
--- /dev/null
+++ b/theories/proofmode/monpred.v
@@ -0,0 +1,363 @@
+From iris.bi Require Export monpred.
+From iris.proofmode Require Import tactics.
+Import MonPred.
+
+Class MakeMonPredCar {I : bi_index} {PROP : bi} (i : I)
+      (P : monPred I PROP) (𝓟 : PROP) :=
+  make_monPred_car : P i ⊣⊢ 𝓟.
+Arguments MakeMonPredCar {_ _} _ _%I _%I.
+Hint Mode MakeMonPredCar + + - ! - : typeclass_instances.
+
+Class IsBiIndexRel {I : bi_index} (i j : I) := is_bi_index_rel : i ⊑ j.
+Hint Mode IsBiIndexRel + - - : typeclass_instances.
+Instance is_bi_index_rel_refl {I : bi_index} (i : I) : IsBiIndexRel i i | 0.
+Proof. by rewrite /IsBiIndexRel. Qed.
+Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
+            : typeclass_instances.
+
+Section bi.
+Context {I : bi_index} {PROP : bi}.
+Local Notation monPred := (monPred I PROP).
+Local Notation MakeMonPredCar := (@MakeMonPredCar I PROP).
+Implicit Types P Q R : monPred.
+Implicit Types 𝓟 𝓠 𝓡 : PROP.
+Implicit Types φ : Prop.
+Implicit Types i j : I.
+
+Global Instance make_monPred_car_pure φ i : MakeMonPredCar i ⌜φ⌝ ⌜φ⌝.
+Proof. rewrite /MakeMonPredCar. by unseal. Qed.
+Global Instance make_monPred_car_internal_eq {A : ofeT} (x y : A) i :
+  MakeMonPredCar i (x ≡ y) (x ≡ y).
+Proof. rewrite /MakeMonPredCar. by unseal. Qed.
+Global Instance make_monPred_car_emp i : MakeMonPredCar i emp emp.
+Proof. rewrite /MakeMonPredCar. by unseal. Qed.
+Global Instance make_monPred_car_sep i P 𝓟 Q 𝓠 :
+  MakeMonPredCar i P 𝓟 → MakeMonPredCar i Q 𝓠 →
+  MakeMonPredCar i (P ∗ Q) (𝓟 ∗ 𝓠).
+Proof. rewrite /MakeMonPredCar=><-<-. by unseal. Qed.
+Global Instance make_monPred_car_and i P 𝓟 Q 𝓠 :
+  MakeMonPredCar i P 𝓟 → MakeMonPredCar i Q 𝓠 →
+  MakeMonPredCar i (P ∧ Q) (𝓟 ∧ 𝓠).
+Proof. rewrite /MakeMonPredCar=><-<-. by unseal. Qed.
+Global Instance make_monPred_car_or i P 𝓟 Q 𝓠 :
+  MakeMonPredCar i P 𝓟 → MakeMonPredCar i Q 𝓠 →
+  MakeMonPredCar i (P ∨ Q) (𝓟 ∨ 𝓠).
+Proof. rewrite /MakeMonPredCar=><-<-. by unseal. Qed.
+Global Instance make_monPred_car_forall {A} i (Φ : A → monPred) (Ψ : A → PROP) :
+  (∀ a, MakeMonPredCar i (Φ a) (Ψ a)) → MakeMonPredCar i (∀ a, Φ a) (∀ a, Ψ a).
+Proof. rewrite /MakeMonPredCar=>H. setoid_rewrite <- H. by unseal. Qed.
+Global Instance make_monPred_car_exists {A} i (Φ : A → monPred) (Ψ : A → PROP) :
+  (∀ a, MakeMonPredCar i (Φ a) (Ψ a)) → MakeMonPredCar i (∃ a, Φ a) (∃ a, Ψ a).
+Proof. rewrite /MakeMonPredCar=>H. setoid_rewrite <- H. by unseal. Qed.
+Global Instance make_monPred_car_persistently i P 𝓟 :
+  MakeMonPredCar i P 𝓟 → MakeMonPredCar i (bi_persistently P) (bi_persistently 𝓟).
+Proof. rewrite /MakeMonPredCar=><-. by unseal. Qed.
+Global Instance make_monPred_car_affinely i P 𝓟 :
+  MakeMonPredCar i P 𝓟 → MakeMonPredCar i (bi_affinely P) (bi_affinely 𝓟).
+Proof. rewrite /MakeMonPredCar=><-. by unseal. Qed.
+Global Instance make_monPred_car_absorbingly i P 𝓟 :
+  MakeMonPredCar i P 𝓟 → MakeMonPredCar i (bi_absorbingly P) (bi_absorbingly 𝓟).
+Proof. rewrite /MakeMonPredCar=><-. by unseal. Qed.
+Global Instance make_monPred_car_persistently_if i P 𝓟 p :
+  MakeMonPredCar i P 𝓟 →
+  MakeMonPredCar i (bi_persistently_if p P) (bi_persistently_if p 𝓟).
+Proof. destruct p; simpl; apply _. Qed.
+Global Instance make_monPred_car_affinely_if i P 𝓟 p :
+  MakeMonPredCar i P 𝓟 →
+  MakeMonPredCar i (bi_affinely_if p P) (bi_affinely_if p 𝓟).
+Proof. destruct p; simpl; apply _. Qed.
+Global Instance make_monPred_car_embed i : MakeMonPredCar i ⎡P⎤ P.
+Proof. rewrite /MakeMonPredCar. by unseal. Qed.
+Global Instance make_monPred_car_in i j : MakeMonPredCar j (monPred_in i) ⌜i ⊑ j⌝.
+Proof. rewrite /MakeMonPredCar. by unseal. Qed.
+Global Instance make_monPred_car_default i P : MakeMonPredCar i P (P i) | 100.
+Proof. by rewrite /MakeMonPredCar. Qed.
+
+Global Instance from_assumption_make_monPred_car_l p i j P 𝓟 :
+  MakeMonPredCar i P 𝓟 → IsBiIndexRel j i → FromAssumption p (P j) 𝓟.
+Proof.
+  rewrite /MakeMonPredCar /FromAssumption /IsBiIndexRel=><- ->.
+  apply  bi.affinely_persistently_if_elim.
+Qed.
+Global Instance from_assumption_make_monPred_car_r p i j P 𝓟 :
+  MakeMonPredCar i P 𝓟 → IsBiIndexRel i j → FromAssumption p 𝓟 (P j).
+Proof.
+  rewrite /MakeMonPredCar /FromAssumption /IsBiIndexRel=><- ->.
+  apply  bi.affinely_persistently_if_elim.
+Qed.
+
+Global Instance as_valid_monPred_car φ P (Φ : I → PROP) :
+  AsValid φ P → (∀ i, MakeMonPredCar i P (Φ i)) → AsValid' φ (∀ i, Φ i) | 100.
+Proof.
+  rewrite /MakeMonPredCar /AsValid' /AsValid /bi_valid=> -> EQ.
+  setoid_rewrite <-EQ. unseal; split.
+  - move=>[/= /bi.forall_intro //].
+  - move=>HP. split=>i. rewrite /= HP bi.forall_elim //.
+Qed.
+Global Instance as_valid_monPred_car_wand φ P Q (Φ Ψ : I → PROP) :
+  AsValid φ (P -∗ Q) →
+  (∀ i, MakeMonPredCar i P (Φ i)) → (∀ i, MakeMonPredCar i Q (Ψ i)) →
+  AsValid' φ (∀ i, Φ i -∗ Ψ i).
+Proof.
+  rewrite /AsValid' /AsValid /MakeMonPredCar. intros -> EQ1 EQ2.
+  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
+  - move=>/bi.wand_entails HP. setoid_rewrite HP. by iIntros (i) "$".
+  - move=>HP. apply bi.entails_wand. split=>i. iIntros "H". by iApply HP.
+Qed.
+Global Instance as_valid_monPred_car_equiv φ P Q (Φ Ψ : I → PROP) :
+  AsValid φ (P ∗-∗ Q) →
+  (∀ i, MakeMonPredCar i P (Φ i)) → (∀ i, MakeMonPredCar i Q (Ψ i)) →
+  AsValid' φ (∀ i, Φ i ∗-∗ Ψ i).
+Proof.
+  rewrite /AsValid' /AsValid /MakeMonPredCar. intros -> EQ1 EQ2.
+  setoid_rewrite <-EQ1. setoid_rewrite <-EQ2. split.
+  - move=>/bi.wand_iff_equiv HP. setoid_rewrite HP. iIntros. iSplit; iIntros "$".
+  - move=>HP. apply bi.equiv_wand_iff. split=>i. by iSplit; iIntros; iApply HP.
+Qed.
+
+Global Instance into_pure_monPred_car P φ i :
+  IntoPure P φ → IntoPure (P i) φ.
+Proof. rewrite /IntoPure=>->. by unseal. Qed.
+Global Instance from_pure_monPred_car P φ i :
+  FromPure P φ → FromPure (P i) φ.
+Proof. rewrite /FromPure=><-. by unseal. Qed.
+Global Instance into_pure_monPred_in i j :
+  @IntoPure PROP (monPred_in i j) (i ⊑ j).
+Proof. rewrite /IntoPure. by unseal. Qed.
+Global Instance from_pure_monPred_in i j :
+  @FromPure PROP (monPred_in i j) (i ⊑ j).
+Proof. rewrite /FromPure. by unseal. Qed.
+
+Global Instance into_internal_eq_monPred_car {A : ofeT} (x y : A) P i :
+  IntoInternalEq P x y → IntoInternalEq (P i) x y.
+Proof. rewrite /IntoInternalEq=> ->. by unseal. Qed.
+
+Global Instance into_persistent_monPred_car p P Q 𝓠 i :
+  IntoPersistent p P Q → MakeMonPredCar i Q 𝓠 → IntoPersistent p (P i) 𝓠 | 0.
+Proof.
+  rewrite /IntoPersistent /MakeMonPredCar /bi_persistently_if.
+  unseal=>-[/(_ i) ?] <-. by destruct p.
+Qed.
+
+Global Instance from_always_monPred_car a pe P Q 𝓠 i :
+  FromAlways a pe false P Q → MakeMonPredCar i Q 𝓠 →
+  FromAlways a pe false (P i) 𝓠 | 0.
+Proof.
+  rewrite /FromAlways /MakeMonPredCar /bi_persistently_if /bi_affinely_if=><-.
+  by destruct a, pe=><-; try unseal.
+Qed.
+
+Lemma into_wand_monPred_car_unknown_unknown p q R P 𝓟 Q 𝓠 i :
+  IntoWand p q R P Q →  MakeMonPredCar i P 𝓟 → MakeMonPredCar i Q 𝓠 →
+  IntoWand p q (R i) 𝓟 𝓠.
+Proof.
+  rewrite /IntoWand /MakeMonPredCar /bi_affinely_if /bi_persistently_if.
+  destruct p, q=> /bi.wand_elim_l' [/(_ i) H] <- <-; apply bi.wand_intro_r;
+  revert H; unseal; done.
+Qed.
+Lemma into_wand_monPred_car_unknown_known p q R P 𝓟 Q i j :
+  IsBiIndexRel i j → IntoWand p q R P Q →
+  MakeMonPredCar j P 𝓟 → IntoWand p q (R i) 𝓟 (Q j).
+Proof.
+  rewrite /IntoWand /IsBiIndexRel /MakeMonPredCar=>-> ? ?.
+  eapply into_wand_monPred_car_unknown_unknown=>//. apply _.
+Qed.
+Lemma into_wand_monPred_car_known_unknown_le p q R P Q 𝓠 i j :
+  IsBiIndexRel i j → IntoWand p q R P Q →
+  MakeMonPredCar j Q 𝓠 → IntoWand p q (R i) (P j) 𝓠.
+Proof.
+  rewrite /IntoWand /IsBiIndexRel /MakeMonPredCar=>-> ? ?.
+  eapply into_wand_monPred_car_unknown_unknown=>//. apply _.
+Qed.
+Lemma into_wand_monPred_car_known_unknown_ge p q R P Q 𝓠 i j :
+  IsBiIndexRel i j → IntoWand p q R P Q →
+  MakeMonPredCar j Q 𝓠 → IntoWand p q (R j) (P i) 𝓠.
+Proof.
+  rewrite /IntoWand /IsBiIndexRel /MakeMonPredCar=>-> ? ?.
+  eapply into_wand_monPred_car_unknown_unknown=>//. apply _.
+Qed.
+
+Global Instance into_wand_wand'_monPred p q P Q 𝓟 𝓠 i :
+  IntoWand' p q ((P -∗ Q) i) 𝓟 𝓠 → IntoWand p q ((P -∗ Q) i) 𝓟 𝓠 | 100.
+Proof. done. Qed.
+Global Instance into_wand_impl'_monPred p q P Q 𝓟 𝓠 i :
+  IntoWand' p q ((P → Q) i) 𝓟 𝓠 → IntoWand p q ((P → Q) i) 𝓟 𝓠 | 100.
+Proof. done. Qed.
+
+Global Instance from_forall_monPred_car_wand P Q (Φ Ψ : I → PROP) i :
+  (∀ j, MakeMonPredCar j P (Φ j)) → (∀ j, MakeMonPredCar j Q (Ψ j)) →
+  FromForall ((P -∗ Q) i)%I (λ j, ⌜i ⊑ j⌝ → Φ j -∗ Ψ j)%I.
+Proof.
+  rewrite /FromForall /MakeMonPredCar. unseal=> H1 H2. do 2 f_equiv.
+  by rewrite H1 H2.
+Qed.
+Global Instance from_forall_monPred_car_impl P Q (Φ Ψ : I → PROP) i :
+  (∀ j, MakeMonPredCar j P (Φ j)) → (∀ j, MakeMonPredCar j Q (Ψ j)) →
+  FromForall ((P → Q) i)%I (λ j, ⌜i ⊑ j⌝ → Φ j → Ψ j)%I.
+Proof.
+  rewrite /FromForall /MakeMonPredCar. unseal=> H1 H2. do 2 f_equiv.
+  by rewrite H1 H2 bi.pure_impl_forall.
+Qed.
+
+Global Instance into_forall_monPred_car_index P i :
+  IntoForall (P i) (λ j, ⌜i ⊑ j⌝ → P j)%I | 100.
+Proof.
+  rewrite /IntoForall. setoid_rewrite bi.pure_impl_forall.
+  do 2 apply bi.forall_intro=>?. by f_equiv.
+Qed.
+
+Global Instance from_and_monPred_car P Q1 𝓠1 Q2 𝓠2 i :
+  FromAnd P Q1 Q2 → MakeMonPredCar i Q1 𝓠1 → MakeMonPredCar i Q2 𝓠2 →
+  FromAnd (P i) 𝓠1 𝓠2.
+Proof. rewrite /FromAnd /MakeMonPredCar /MakeMonPredCar=> <- <- <-. by unseal. Qed.
+Global Instance into_and_monPred_car p P Q1 𝓠1 Q2 𝓠2 i :
+  IntoAnd p P Q1 Q2 → MakeMonPredCar i Q1 𝓠1 → MakeMonPredCar i Q2 𝓠2 →
+  IntoAnd p (P i) 𝓠1 𝓠2.
+Proof.
+  rewrite /IntoAnd /MakeMonPredCar /bi_affinely_if /bi_persistently_if.
+  destruct p=>-[/(_ i) H] <- <-; revert H; unseal; done.
+Qed.
+
+Global Instance from_sep_monPred_car P Q1 𝓠1 Q2 𝓠2 i :
+  FromSep P Q1 Q2 → MakeMonPredCar i Q1 𝓠1 → MakeMonPredCar i Q2 𝓠2 →
+  FromSep (P i) 𝓠1 𝓠2.
+Proof. rewrite /FromSep /MakeMonPredCar=> <- <- <-. by unseal. Qed.
+Global Instance into_sep_monPred_car P Q1 𝓠1 Q2 𝓠2 i :
+  IntoSep P Q1 Q2 → MakeMonPredCar i Q1 𝓠1 → MakeMonPredCar i Q2 𝓠2 →
+  IntoSep (P i) 𝓠1 𝓠2.
+Proof. rewrite /IntoSep /MakeMonPredCar=> -> <- <-. by unseal. Qed.
+
+Global Instance from_or_monPred_car P Q1 𝓠1 Q2 𝓠2 i :
+  FromOr P Q1 Q2 → MakeMonPredCar i Q1 𝓠1 → MakeMonPredCar i Q2 𝓠2 →
+  FromOr (P i) 𝓠1 𝓠2.
+Proof. rewrite /FromOr /MakeMonPredCar=> <- <- <-. by unseal. Qed.
+Global Instance into_or_monPred_car P Q1 𝓠1 Q2 𝓠2 i :
+  IntoOr P Q1 Q2 → MakeMonPredCar i Q1 𝓠1 → MakeMonPredCar i Q2 𝓠2 →
+  IntoOr (P i) 𝓠1 𝓠2.
+Proof. rewrite /IntoOr /MakeMonPredCar=> -> <- <-. by unseal. Qed.
+
+Global Instance from_exist_monPred_car {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
+  FromExist P Φ → (∀ a, MakeMonPredCar i (Φ a) (Ψ a)) → FromExist (P i) Ψ.
+Proof.
+  rewrite /FromExist /MakeMonPredCar=><- H. setoid_rewrite <- H. by unseal.
+Qed.
+Global Instance into_exist_monPred_car {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
+  IntoExist P Φ → (∀ a, MakeMonPredCar i (Φ a) (Ψ a)) → IntoExist (P i) Ψ.
+Proof.
+  rewrite /IntoExist /MakeMonPredCar=>-> H. setoid_rewrite <- H. by unseal.
+Qed.
+
+Global Instance foram_forall_monPred_car_plainly i P Φ :
+  (∀ i, MakeMonPredCar i P (Φ i)) →
+  FromForall (bi_plainly P i) (λ j, bi_plainly (Φ j)).
+Proof. rewrite /FromForall /MakeMonPredCar=>H. unseal. do 3 f_equiv. rewrite H //. Qed.
+Global Instance into_forall_monPred_car_plainly i P Φ :
+  (∀ i, MakeMonPredCar i P (Φ i)) →
+  IntoForall (bi_plainly P i) (λ j, bi_plainly (Φ j)).
+Proof. rewrite /IntoForall /MakeMonPredCar=>H. unseal. do 3 f_equiv. rewrite H //. Qed.
+
+Global Instance from_forall_monPred_car_all P (Φ : I → PROP) i :
+  (∀ i, MakeMonPredCar i P (Φ i)) → FromForall (monPred_all P i) Φ.
+Proof.
+  rewrite /FromForall /MakeMonPredCar=>H. setoid_rewrite <- H. by unseal.
+Qed.
+Global Instance into_forall_monPred_car_all P (Φ : I → PROP) i :
+  (∀ i, MakeMonPredCar i P (Φ i)) → IntoForall (monPred_all P i) Φ.
+Proof.
+  rewrite /IntoForall /MakeMonPredCar=>H. setoid_rewrite <- H. by unseal.
+Qed.
+
+Global Instance from_forall_monPred_car {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
+  FromForall P Φ → (∀ a, MakeMonPredCar i (Φ a) (Ψ a)) → FromForall (P i) Ψ.
+Proof.
+  rewrite /FromForall /MakeMonPredCar=><- H. setoid_rewrite <- H. by unseal.
+Qed.
+Global Instance into_forall_monPred_car {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
+  IntoForall P Φ → (∀ a, MakeMonPredCar i (Φ a) (Ψ a)) → IntoForall (P i) Ψ.
+Proof.
+  rewrite /IntoForall /MakeMonPredCar=>-> H. setoid_rewrite <- H. by unseal.
+Qed.
+
+(* FIXME : there are two good ways to frame under a call to
+   monPred_car. This may cause some backtracking in the typeclass
+   search, and hence performance issues. *)
+Global Instance frame_monPred_car p P Q 𝓠 R i j :
+  IsBiIndexRel i j → Frame p R P Q → MakeMonPredCar j Q 𝓠 →
+  Frame p (R i) (P j) 𝓠.
+Proof.
+  rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if
+          /IsBiIndexRel=> Hij <- <-.
+  by destruct p; rewrite Hij; unseal.
+Qed.
+Global Instance frame_monPred_car_embed i p P Q 𝓠 𝓡 :
+  Frame p ⎡𝓡⎤ P Q → MakeMonPredCar i Q 𝓠 → Frame p 𝓡 (P i) 𝓠.
+Proof.
+  rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if=> <- <-.
+  by destruct p; unseal.
+Qed.
+
+Global Instance from_modal_monPred_car i P Q 𝓠 :
+  FromModal P Q → MakeMonPredCar i Q 𝓠 → FromModal (P i) 𝓠.
+Proof. by rewrite /FromModal /MakeMonPredCar=> <- <-. Qed.
+End bi.
+
+(* When P and/or Q are evars when doing typeclass search on [IntoWand
+   (R i) P Q], we use [MakeMonPredCar] in order to normalize the
+   result of unification. However, when they are not evars, we want to
+   propagate the known information through typeclass search. Hence, we
+   do not want to use [MakeMonPredCar].
+
+   As a result, depending on P and Q being evars, we use a different
+   version of [into_wand_monPred_car_xx_xx]. *)
+Hint Extern 3 (IntoWand _ _ (monPred_car _ _) ?P ?Q) =>
+     is_evar P; is_evar Q;
+     eapply @into_wand_monPred_car_unknown_unknown
+     : typeclass_instances.
+Hint Extern 2 (IntoWand _ _ (monPred_car _ _) ?P (monPred_car ?Q _)) =>
+     eapply @into_wand_monPred_car_unknown_known
+     : typeclass_instances.
+Hint Extern 2 (IntoWand _ _ (monPred_car _ _) (monPred_car ?P _) ?Q) =>
+     eapply @into_wand_monPred_car_known_unknown_le
+     : typeclass_instances.
+Hint Extern 2 (IntoWand _ _ (monPred_car _ _) (monPred_car ?P _) ?Q) =>
+     eapply @into_wand_monPred_car_known_unknown_ge
+     : typeclass_instances.
+
+Section sbi.
+Context {I : bi_index} {PROP : sbi}.
+Local Notation monPred := (monPred I PROP).
+Implicit Types P Q R : monPred.
+Implicit Types 𝓟 𝓠 𝓡 : PROP.
+Implicit Types φ : Prop.
+Implicit Types i j : I.
+
+Global Instance is_except_0_monPred_car i P :
+  IsExcept0 P → IsExcept0 (P i).
+Proof. rewrite /IsExcept0=>- [/(_ i)]. by unseal. Qed.
+
+Global Instance make_monPred_car_except_0 i P 𝓠 :
+  MakeMonPredCar i P 𝓠 → MakeMonPredCar i (◇ P)%I (◇ 𝓠)%I.
+Proof. rewrite /MakeMonPredCar=><-. by unseal. Qed.
+Global Instance make_monPred_car_later i P 𝓠 :
+  MakeMonPredCar i P 𝓠 → MakeMonPredCar i (▷ P)%I (▷ 𝓠)%I.
+Proof. rewrite /MakeMonPredCar=><-. by unseal. Qed.
+Global Instance make_monPred_car_laterN i n P 𝓠 :
+  MakeMonPredCar i P 𝓠 → MakeMonPredCar i (▷^n P)%I (▷^n 𝓠)%I.
+Proof. rewrite /MakeMonPredCar=> <-. elim n=>//= ? <-. by unseal. Qed.
+
+Global Instance into_except_0_monPred_car_fwd i P Q 𝓠 :
+  IntoExcept0 P Q → MakeMonPredCar i Q 𝓠 → IntoExcept0 (P i) 𝓠.
+Proof. rewrite /IntoExcept0 /MakeMonPredCar=> -> <-. by unseal. Qed.
+Global Instance into_except_0_monPred_car_bwd i P 𝓟 Q :
+  IntoExcept0 P Q → MakeMonPredCar i P 𝓟 → IntoExcept0 𝓟 (Q i).
+Proof. rewrite /IntoExcept0 /MakeMonPredCar=> H <-. rewrite H. by unseal. Qed.
+
+Global Instance into_later_monPred_car i n P Q 𝓠 :
+  IntoLaterN n P Q → MakeMonPredCar i Q 𝓠 → IntoLaterN n (P i) 𝓠.
+Proof.
+  rewrite /IntoLaterN /MakeMonPredCar=> -> <-. elim n=>//= ? <-. by unseal.
+Qed.
+Global Instance from_later_monPred_car i n P Q 𝓠 :
+  FromLaterN n P Q → MakeMonPredCar i Q 𝓠 → FromLaterN n (P i) 𝓠.
+Proof. rewrite /FromLaterN /MakeMonPredCar=> <- <-. elim n=>//= ? ->. by unseal. Qed.
+End sbi.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 09b1b98c96bf7ddccccafaba4d92d23878631f35..ff7858d035f8a98326fa3512c22daf76b3198634 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -65,22 +65,39 @@ Proof. by apply as_valid. Qed.
 Instance as_valid_valid {PROP : bi} (P : PROP) : AsValid (bi_valid P) P | 0.
 Proof. by rewrite /AsValid. Qed.
 
-Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid (P ⊢ Q) (P -∗ Q) | 1.
+Instance as_valid_entails {PROP : bi} (P Q : PROP) : AsValid (P ⊢ Q) (P -∗ Q) | 0.
 Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
 
-Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid (P ≡ Q) (P ∗-∗ Q).
+Instance as_valid_equiv {PROP : bi} (P Q : PROP) : AsValid (P ≡ Q) (P ∗-∗ Q) | 0.
 Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
 
+Class AsValid' {PROP : bi} (φ : Prop) (P : PROP) := as_valid' :> AsValid φ P.
+Arguments AsValid' {_} _%type _%I.
+Hint Mode AsValid' ! ! - : typeclass_instances.
+
+Instance as_valid_embed `{BiEmbedding PROP PROP'} (φ : Prop) (P : PROP) :
+  AsValid φ P → AsValid' φ ⎡P⎤.
+Proof. rewrite /AsValid' /AsValid=> ->. rewrite bi_embed_valid //. Qed.
+
 (** * Start a proof *)
-Ltac iStartProof :=
+Tactic Notation "iStartProof" uconstr(PROP) :=
   lazymatch goal with
-  | |- envs_entails _ _ => idtac
+  | |- @envs_entails ?PROP' _ _ =>
+    let x := type_term (eq_refl : @eq Type PROP PROP') in idtac
   | |- let _ := _ in _ => fail
-  | |- ?φ => eapply (as_valid_2 φ);
+
+  (* We eta-expand [as_valid_2], in order to make sure that
+     [iStartProof works] even if [PROP] is the carrier type. In this
+     case, typing this expression will end up unifying PROP with
+     [bi_car _], and hence trigger the canonical structures mechanism
+     to find the corresponding bi. *)
+  | |- ?φ => eapply (λ P : PROP, @as_valid_2 φ _ P);
                [apply _ || fail "iStartProof: not a Bi entailment"
                |apply tac_adequate]
   end.
 
+Tactic Notation "iStartProof" := iStartProof _.
+
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
   eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index ec136a553766ebe890b304ab87e38872e93276aa..f22e3838ee11d88973c94d78cc60d124ee9878f4 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -36,6 +36,15 @@ Section base_logic_tests.
 
   Lemma test_iAssert_modality P : (|==> False) -∗ |==> P.
   Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.
+
+  Lemma test_iStartProof_1 P : P -∗ P.
+  Proof. iStartProof. iStartProof. iIntros "$". Qed.
+  Lemma test_iStartProof_2 P : P -∗ P.
+  Proof. iStartProof (uPred _). iStartProof (uPredI _). iIntros "$". Qed.
+  Lemma test_iStartProof_3 P : P -∗ P.
+  Proof. iStartProof (uPredI _). iStartProof (uPredSI _). iIntros "$". Qed.
+  Lemma test_iStartProof_4 P : P -∗ P.
+  Proof. iStartProof (uPredSI _). iStartProof (uPred _). iIntros "$". Qed.
 End base_logic_tests.
 
 Section iris_tests.
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
new file mode 100644
index 0000000000000000000000000000000000000000..a18ce8ef0eeeb5d60a23538a274dd37c4b9a921f
--- /dev/null
+++ b/theories/tests/proofmode_monpred.v
@@ -0,0 +1,53 @@
+From iris.proofmode Require Import tactics monpred.
+From iris.base_logic Require Import base_logic lib.invariants.
+
+Section tests.
+  Context {I : bi_index} {PROP : sbi}.
+  Local Notation monPred := (monPred I PROP).
+  Local Notation monPredI := (monPredI I PROP).
+  Local Notation monPredSI := (monPredSI I PROP).
+  Implicit Types P Q R : monPred.
+  Implicit Types i j : I.
+
+  Lemma test0 P : P -∗ P.
+  Proof. iIntros "$". Qed.
+
+  Lemma test_iStartProof_1 P : P -∗ P.
+  Proof. iStartProof. iStartProof. iIntros "$". Qed.
+  Lemma test_iStartProof_2 P : P -∗ P.
+  Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
+  Lemma test_iStartProof_3 P : P -∗ P.
+  Proof. iStartProof monPredI. iStartProof monPredSI. iIntros "$". Qed.
+  Lemma test_iStartProof_4 P : P -∗ P.
+  Proof. iStartProof monPredSI. iStartProof monPred. iIntros "$". Qed.
+  Lemma test_iStartProof_5 P : P -∗ P.
+  Proof. iStartProof PROP. iIntros (i) "$". Qed.
+  Lemma test_iStartProof_6 P : P ⊣⊢ P.
+  Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
+  Lemma test_iStartProof_7 P : ((P ≡ P)%I : monPredI).
+  Proof. iStartProof PROP. done. Qed.
+
+  Lemma test_intowand_1 P Q : (P -∗ Q) -∗ P -∗ Q.
+  Proof.
+    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". by iApply "HW".
+  Qed.
+  Lemma test_intowand_2 P Q : (P -∗ Q) -∗ P -∗ Q.
+  Proof.
+    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
+    iSpecialize ("HW" with "[HP //]"). done.
+  Qed.
+  Lemma test_intowand_3 P Q : (P -∗ Q) -∗ P -∗ Q.
+  Proof.
+    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
+    iSpecialize ("HW" with "HP"). done.
+  Qed.
+  Lemma test_intowand_4 P Q : (P -∗ Q) -∗ ▷ P -∗ ▷ Q.
+  Proof.
+    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". by iApply "HW".
+  Qed.
+  Lemma test_intowand_5 P Q : (P -∗ Q) -∗ ▷ P -∗ ▷ Q.
+  Proof.
+    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
+    iSpecialize ("HW" with "HP"). done.
+  Qed.
+End tests.