diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c9f39a47c57cfba6d1df46f9fb41cce104fd667e..d9e42bee2135f0eda69d694df9f6ed97db37fee6 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -739,8 +739,8 @@ Qed.
 Class MakeMorphism `{BiEmbedding PROP PROP'} P (Q : PROP') :=
   make_embed : ⎡P⎤ ⊣⊢ Q.
 Arguments MakeMorphism {_ _ _} _%I _%I.
-Global Instance make_embed_true `{BiEmbedding PROP PROP'} :
-  MakeMorphism True True.
+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.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 992a6342fb4bc314bd2d86e9a4eb4e4d0d6ffd0d..53601d0306c6ddc1d20b6adbdce17d70e9959bf2 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -6,147 +6,218 @@ Section bi.
 Context {I : bi_index} {PROP : bi}.
 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 as_valid_monPred_car φ P :
-  AsValid φ P → AsValid φ (∀ i, P i).
+Class MakeMonPredCar i P 𝓟 :=
+  make_monPred_car : P i ⊣⊢ 𝓟.
+Arguments MakeMonPredCar _ _%I _%I.
+
+Global Instance make_monPred_car_pure φ i : MakeMonPredCar i ⌜φ⌝ ⌜φ⌝.
+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_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 as_valid_monPred_car φ P (Φ : I → PROP) :
+  AsValid φ P → (∀ i, MakeMonPredCar i P (Φ i)) → AsValid φ (∀ i, Φ i).
 Proof.
-  rewrite /AsValid /bi_valid=> ->; unseal; split.
+  rewrite /MakeMonPredCar /AsValid /bi_valid=> -> EQ. setoid_rewrite <-EQ.
+  unseal; split.
   - move=>[/= /bi.forall_intro //].
   - move=>H. split=>i. rewrite /= H bi.forall_elim //.
 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_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 → IntoPersistent p (P i) (Q i) | 0.
+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 /bi_persistently_if. unseal=>-[/(_ i)].
-  by destruct p.
+  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 → FromAlways a pe false (P i) (Q i) | 0.
+
+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 /bi_persistently_if /bi_affinely_if=><-.
-  by destruct a, pe; try unseal.
+  rewrite /FromAlways /MakeMonPredCar /bi_persistently_if /bi_affinely_if=><-.
+  by destruct a, pe=><-; try unseal.
 Qed.
 
-Global Instance into_wand_monPred_car p q R P Q i :
-  IntoWand p q R P Q → IntoWand p q (R i) (P i) (Q i).
+Global Instance into_wand_monPred_car 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 /bi_affinely_if /bi_persistently_if=>/bi.wand_elim_l' <-.
-  apply bi.wand_intro_r. by destruct p, q; unseal.
+  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.
+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.
+  setoid_rewrite H1. setoid_rewrite H2. done.
+Qed.
+Global Instance into_forall_monPred_car_wand P Q (Φ Ψ : I → PROP) i :
+  (∀ j, MakeMonPredCar j P (Φ j)) → (∀ j, MakeMonPredCar j Q (Ψ j)) →
+  IntoForall ((P -∗ Q) i) (λ j, ⌜i ⊑ j⌝ → Φ j -∗ Ψ j)%I.
+Proof.
+  rewrite /IntoForall /MakeMonPredCar. unseal=> H1 H2.
+  setoid_rewrite H1. setoid_rewrite H2. done.
+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.
+  setoid_rewrite H1. setoid_rewrite H2. done.
+Qed.
+Global Instance into_forall_monPred_car_impl P Q (Φ Ψ : I → PROP) i :
+  (∀ j, MakeMonPredCar j P (Φ j)) → (∀ j, MakeMonPredCar j Q (Ψ j)) →
+  IntoForall ((P → Q) i) (λ j, ⌜i ⊑ j⌝ → Φ j → Ψ j)%I.
+Proof.
+  rewrite /IntoForall /MakeMonPredCar. unseal=> H1 H2.
+  setoid_rewrite H1. setoid_rewrite H2. done.
 Qed.
-Global Instance from_forall_monPred_car_wand P Q i :
-  FromForall ((P -∗ Q) i)%I (λ j, ⌜i ⊑ j⌝ → P j -∗ Q j)%I.
-Proof. rewrite /FromForall. by unseal. Qed.
-Global Instance into_forall_monPred_car_wand P Q i :
-  IntoForall ((P -∗ Q) i) (λ j, ⌜i ⊑ j⌝ → P j -∗ Q j)%I.
-Proof. rewrite /IntoForall. by unseal. Qed.
-Global Instance from_forall_monPred_car_impl P Q i :
-  FromForall ((P → Q) i)%I (λ j, ⌜i ⊑ j⌝ → P j → Q j)%I.
-Proof. rewrite /FromForall. by unseal. Qed.
-Global Instance into_forall_monPred_car_impl P Q i :
-  IntoForall ((P → Q) i) (λ j, ⌜i ⊑ j⌝ → P j → Q j)%I.
-Proof. rewrite /IntoForall. by unseal. Qed.
 
-Global Instance from_and_monPred_car P Q1 Q2 i:
-  FromAnd P Q1 Q2 → FromAnd (P i) (Q1 i) (Q2 i).
-Proof. rewrite /FromAnd=> <-. by unseal. Qed.
-Global Instance into_and_monPred_car p P Q1 Q2 i:
-  IntoAnd p P Q1 Q2 → IntoAnd p (P i) (Q1 i) (Q2 i).
+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 /bi_affinely_if /bi_persistently_if=>-[/(_ i)].
-  by destruct p; unseal.
+  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 Q2 i:
-  FromSep P Q1 Q2 → FromSep (P i) (Q1 i) (Q2 i).
-Proof. rewrite /FromSep=> <-. by unseal. Qed.
-Global Instance into_sep_monPred_car P Q1 Q2 i:
-  IntoSep P Q1 Q2 → IntoSep (P i) (Q1 i) (Q2 i).
-Proof. rewrite /IntoSep=> ->. by unseal. Qed.
-
-Global Instance from_or_monPred_car P Q1 Q2 i:
-  FromOr P Q1 Q2 → FromOr (P i) (Q1 i) (Q2 i).
-Proof. rewrite /FromOr=> <-. by unseal. Qed.
-Global Instance into_or_monPred_car P Q1 Q2 i:
-  IntoOr P Q1 Q2 → IntoOr (P i) (Q1 i) (Q2 i).
-Proof. rewrite /IntoOr=> ->. by unseal. Qed.
-
-Global Instance from_exist_monPred_car {A} P (Φ : A → monPred) i :
-  FromExist P Φ → FromExist (P i) (λ a, Φ a i).
-Proof. rewrite /FromExist=><-. by unseal. Qed.
-Global Instance into_exist_monPred_car {A} P (Φ : A → monPred) i :
-  IntoExist P Φ → IntoExist (P i) (λ a, Φ a i).
-Proof. rewrite /IntoExist=>->. by unseal. Qed.
-
-Global Instance from_forall_monPred_car {A} P (Φ : A → monPred) i :
-  FromForall P Φ → FromForall (P i) (λ a, Φ a i).
-Proof. rewrite /FromForall=><-. by unseal. Qed.
-Global Instance into_forall_monPred_car {A} P (Φ : A → monPred) i :
-  IntoForall P Φ → IntoForall (P i) (λ a, Φ a i).
-Proof. rewrite /IntoForall=>->. by unseal. Qed.
-
-Class MakeMonPredCar i P (Q : PROP) :=
-  make_monPred_car : P i ⊣⊢ Q.
-Arguments MakeMonPredCar _ _%I _%I.
-Global Instance make_monPred_car_true i : MakeMonPredCar i True True.
-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_default i P : MakeMonPredCar i P (P i).
-Proof. by rewrite /MakeMonPredCar. 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 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.
+
+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.
 
 (* 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 i p P Q (Q' : PROP) R :
-  Frame p R P Q → MakeMonPredCar i Q Q' → Frame p (R i) (P i) Q'.
+Global Instance frame_monPred_car i p P Q 𝓠 R :
+  Frame p R P Q → MakeMonPredCar i Q 𝓠 → Frame p (R i) (P i) 𝓠.
 Proof.
   rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if=> <- <-.
   by destruct p; unseal.
 Qed.
-Global Instance frame_monPred_car_embed i p P Q (Q' R: PROP) :
-  Frame p ⎡R⎤ P Q → MakeMonPredCar i Q Q' → Frame p R (P i) Q'.
+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 → FromModal (P i) (Q i).
-Proof. by rewrite /FromModal=>->. 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.
 
+Hint Mode MakeMonPredCar + + - ! -.
+
 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 into_except_0_monPred_car i P Q :
-  IntoExcept0 P Q → IntoExcept0 (P i) (Q i).
-Proof. rewrite /IntoExcept0=> ->. by unseal. Qed.
-Global Instance into_later_monPred_car i n P Q :
-  IntoLaterN n P Q → IntoLaterN n (P i) (Q i).
+
+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=> ->. induction n as [|? IH]=>//. rewrite /= -IH. by unseal.
+  rewrite /IntoLaterN /MakeMonPredCar=> -> <-.
+  induction n as [|? IH]=>//. rewrite /= -IH. by unseal.
 Qed.
-Global Instance from_later_monPred_car i n P Q :
-  FromLaterN n P Q → FromLaterN n (P i) (Q i).
+Global Instance from_later_monPred_car i n P Q 𝓠 :
+  FromLaterN n P Q → MakeMonPredCar i Q 𝓠 → FromLaterN n (P i) 𝓠.
 Proof.
-  rewrite /FromLaterN=> <-. induction n as [|? IH]=>//. rewrite /= IH. by unseal.
+  rewrite /FromLaterN /MakeMonPredCar=> <- <-.
+  induction n as [|? IH]=>//. rewrite /= IH. by unseal.
 Qed.
 End sbi.