diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 0a355aa93aaec0d31c2b66862bd9e49e01041873..6821c6aa0447a636fa79de9970afd5f8225fdeeb 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -16,8 +16,8 @@ Context {I : bi_index} {PROP : bi}.
 Implicit Types i : I.
 
 Record monPred :=
-  MonPred { monPred_car :> I â†’ PROP;
-            monPred_mono : Proper ((âŠ‘) ==> (âŠ¢)) monPred_car }.
+  MonPred { monPred_at :> I â†’ PROP;
+            monPred_mono : Proper ((âŠ‘) ==> (âŠ¢)) monPred_at }.
 Local Existing Instance monPred_mono.
 
 Implicit Types P Q : monPred.
@@ -33,7 +33,7 @@ Section Ofe_Cofe_def.
   Instance monPred_dist : Dist monPred := monPred_dist'.
 
   Definition monPred_sig P : { f : I -c> PROP | Proper ((âŠ‘) ==> (âŠ¢)) f } :=
-    exist _ (monPred_car P) (monPred_mono P).
+    exist _ (monPred_at P) (monPred_mono P).
 
   Definition sig_monPred (P' : { f : I -c> PROP | Proper ((âŠ‘) ==> (âŠ¢)) f })
     : monPred :=
@@ -56,7 +56,7 @@ Section Ofe_Cofe_def.
 
   Global Instance monPred_cofe `{Cofe PROP} : Cofe monPredC.
   Proof.
-    unshelve refine (iso_cofe_subtype (A:=I-c>PROP) _ MonPred monPred_car _ _ _);
+    unshelve refine (iso_cofe_subtype (A:=I-c>PROP) _ MonPred monPred_at _ _ _);
       [apply _|by apply monPred_sig_dist|done|].
     intros c i j Hij. apply @limit_preserving;
       [by apply bi.limit_preserving_entails; intros ??|]=>n. by rewrite Hij.
@@ -83,21 +83,21 @@ Proof. eapply (ne_proper _). Qed.
    equivalence relation (and Coq is able to infer the Proper and
    Reflexive instances properly), or any other equivalence relation,
    provided it is compatible with (âŠ‘). *)
-Global Instance monPred_car_ne (R : relation I) :
+Global Instance monPred_at_ne (R : relation I) :
   Proper (R ==> R ==> iff) (âŠ‘) â†’ Reflexive R â†’
-  âˆ€ n, Proper (dist n ==> R ==> dist n) monPred_car.
+  âˆ€ n, Proper (dist n ==> R ==> dist n) monPred_at.
 Proof.
   intros ????? [Hd] ?? HR. rewrite Hd.
   apply equiv_dist, bi.equiv_spec; split; f_equiv; rewrite ->HR; done.
 Qed.
-Global Instance monPred_car_proper (R : relation I) :
+Global Instance monPred_at_proper (R : relation I) :
   Proper (R ==> R ==> iff) (âŠ‘) â†’ Reflexive R â†’
-  Proper ((â‰¡) ==> R ==> (â‰¡)) monPred_car.
+  Proper ((â‰¡) ==> R ==> (â‰¡)) monPred_at.
 Proof. repeat intro. apply equiv_dist=>?. f_equiv=>//. by apply equiv_dist. Qed.
 End Ofe_Cofe.
 
 Arguments monPred _ _ : clear implicits.
-Arguments monPred_car {_ _} _%I _.
+Arguments monPred_at {_ _} _%I _.
 Local Existing Instance monPred_mono.
 Arguments monPredC _ _ : clear implicits.
 
@@ -366,11 +366,11 @@ Context {I : bi_index} {PROP : bi}.
 Implicit Types i : I.
 Implicit Types P Q : monPred I PROP.
 
-Global Instance monPred_car_mono :
-  Proper ((âŠ¢) ==> (âŠ‘) ==> (âŠ¢)) (@monPred_car I PROP).
+Global Instance monPred_at_mono :
+  Proper ((âŠ¢) ==> (âŠ‘) ==> (âŠ¢)) (@monPred_at I PROP).
 Proof. by move=> ?? [?] ?? ->. Qed.
-Global Instance monPred_car_mono_flip :
-  Proper (flip (âŠ¢) ==> flip (âŠ‘) ==> flip (âŠ¢)) (@monPred_car I PROP).
+Global Instance monPred_at_mono_flip :
+  Proper (flip (âŠ¢) ==> flip (âŠ‘) ==> flip (âŠ¢)) (@monPred_at I PROP).
 Proof. solve_proper. Qed.
 
 Global Instance monPred_in_proper (R : relation I) :
@@ -414,7 +414,7 @@ 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) :
+Lemma monPred_at_embed (P : PROP) (i : I) :
   (bi_embed (B := monPred _ _) P) i âŠ£âŠ¢ P.
 Proof. by unseal. Qed.
 
@@ -426,13 +426,13 @@ Lemma monPred_affinely_if_eq p P i:
   (bi_affinely_if p P) i = bi_affinely_if p (P i).
 Proof. rewrite /bi_affinely_if. destruct p => //. rewrite /bi_affinely. by unseal. Qed.
 
-Global Instance monPred_car_persistent P i : Persistent P â†’ Persistent (P i).
+Global Instance monPred_at_persistent P i : Persistent P â†’ Persistent (P i).
 Proof. move => [] /(_ i). by unseal. Qed.
-Global Instance monPred_car_plain P i : Plain P â†’ Plain (P i).
+Global Instance monPred_at_plain P i : Plain P â†’ Plain (P i).
 Proof. move => [] /(_ i). unfold Plain. unseal. rewrite bi.forall_elim //. Qed.
-Global Instance monPred_car_absorbing P i : Absorbing P â†’ Absorbing (P i).
+Global Instance monPred_at_absorbing P i : Absorbing P â†’ Absorbing (P i).
 Proof. move => [] /(_ i). unfold Absorbing. by unseal. Qed.
-Global Instance monPred_car_affine P i : Affine P â†’ Affine (P i).
+Global Instance monPred_at_affine P i : Affine P â†’ Affine (P i).
 Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
 
 (* Note that monPred_in is *not* Plain, because it does depend on the
@@ -487,7 +487,7 @@ Context {I : bi_index} {PROP : sbi}.
 Implicit Types i : I.
 Implicit Types P Q : monPred I PROP.
 
-Global Instance monPred_car_timeless P i : Timeless P â†’ Timeless (P i).
+Global Instance monPred_at_timeless P i : Timeless P â†’ Timeless (P i).
 Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
 Global Instance monPred_embed_timeless (P : PROP) :
   Timeless P â†’ @Timeless (monPredSI I PROP) âŽ¡PâŽ¤%I.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index a3afd86cccd638e56591cc6bf94e26c74decdd89..def9395424ab08e3bee0d9308fbc41264a44fd66 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -2,11 +2,11 @@ From iris.bi Require Export monpred.
 From iris.proofmode Require Import tactics.
 Import MonPred.
 
-Class MakeMonPredCar {I : bi_index} {PROP : bi} (i : I)
+Class MakeMonPredAt {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.
+  make_monPred_at : P i âŠ£âŠ¢ ð“Ÿ.
+Arguments MakeMonPredAt {_ _} _ _%I _%I.
+Hint Mode MakeMonPredAt + + - ! - : typeclass_instances.
 
 Class IsBiIndexRel {I : bi_index} (i j : I) := is_bi_index_rel : i âŠ‘ j.
 Hint Mode IsBiIndexRel + - - : typeclass_instances.
@@ -18,107 +18,107 @@ Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
 Section bi.
 Context {I : bi_index} {PROP : bi}.
 Local Notation monPred := (monPred I PROP).
-Local Notation MakeMonPredCar := (@MakeMonPredCar I PROP).
+Local Notation MakeMonPredAt := (@MakeMonPredAt 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 ð“Ÿ).
+Global Instance make_monPred_at_pure Ï† i : MakeMonPredAt i âŒœÏ†âŒ âŒœÏ†âŒ.
+Proof. rewrite /MakeMonPredAt. by unseal. Qed.
+Global Instance make_monPred_at_internal_eq {A : ofeT} (x y : A) i :
+  MakeMonPredAt i (x â‰¡ y) (x â‰¡ y).
+Proof. rewrite /MakeMonPredAt. by unseal. Qed.
+Global Instance make_monPred_at_emp i : MakeMonPredAt i emp emp.
+Proof. rewrite /MakeMonPredAt. by unseal. Qed.
+Global Instance make_monPred_at_sep i P ð“Ÿ Q ð“  :
+  MakeMonPredAt i P ð“Ÿ â†’ MakeMonPredAt i Q ð“  â†’
+  MakeMonPredAt i (P âˆ— Q) (ð“Ÿ âˆ— ð“ ).
+Proof. rewrite /MakeMonPredAt=><-<-. by unseal. Qed.
+Global Instance make_monPred_at_and i P ð“Ÿ Q ð“  :
+  MakeMonPredAt i P ð“Ÿ â†’ MakeMonPredAt i Q ð“  â†’
+  MakeMonPredAt i (P âˆ§ Q) (ð“Ÿ âˆ§ ð“ ).
+Proof. rewrite /MakeMonPredAt=><-<-. by unseal. Qed.
+Global Instance make_monPred_at_or i P ð“Ÿ Q ð“  :
+  MakeMonPredAt i P ð“Ÿ â†’ MakeMonPredAt i Q ð“  â†’
+  MakeMonPredAt i (P âˆ¨ Q) (ð“Ÿ âˆ¨ ð“ ).
+Proof. rewrite /MakeMonPredAt=><-<-. by unseal. Qed.
+Global Instance make_monPred_at_forall {A} i (Î¦ : A â†’ monPred) (Î¨ : A â†’ PROP) :
+  (âˆ€ a, MakeMonPredAt i (Î¦ a) (Î¨ a)) â†’ MakeMonPredAt i (âˆ€ a, Î¦ a) (âˆ€ a, Î¨ a).
+Proof. rewrite /MakeMonPredAt=>H. setoid_rewrite <- H. by unseal. Qed.
+Global Instance make_monPred_at_exists {A} i (Î¦ : A â†’ monPred) (Î¨ : A â†’ PROP) :
+  (âˆ€ a, MakeMonPredAt i (Î¦ a) (Î¨ a)) â†’ MakeMonPredAt i (âˆƒ a, Î¦ a) (âˆƒ a, Î¨ a).
+Proof. rewrite /MakeMonPredAt=>H. setoid_rewrite <- H. by unseal. Qed.
+Global Instance make_monPred_at_persistently i P ð“Ÿ :
+  MakeMonPredAt i P ð“Ÿ â†’ MakeMonPredAt i (bi_persistently P) (bi_persistently ð“Ÿ).
+Proof. rewrite /MakeMonPredAt=><-. by unseal. Qed.
+Global Instance make_monPred_at_affinely i P ð“Ÿ :
+  MakeMonPredAt i P ð“Ÿ â†’ MakeMonPredAt i (bi_affinely P) (bi_affinely ð“Ÿ).
+Proof. rewrite /MakeMonPredAt=><-. by unseal. Qed.
+Global Instance make_monPred_at_absorbingly i P ð“Ÿ :
+  MakeMonPredAt i P ð“Ÿ â†’ MakeMonPredAt i (bi_absorbingly P) (bi_absorbingly ð“Ÿ).
+Proof. rewrite /MakeMonPredAt=><-. by unseal. Qed.
+Global Instance make_monPred_at_persistently_if i P ð“Ÿ p :
+  MakeMonPredAt i P ð“Ÿ â†’
+  MakeMonPredAt 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 ð“Ÿ).
+Global Instance make_monPred_at_affinely_if i P ð“Ÿ p :
+  MakeMonPredAt i P ð“Ÿ â†’
+  MakeMonPredAt 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 make_monPred_at_embed i : MakeMonPredAt i âŽ¡PâŽ¤ P.
+Proof. rewrite /MakeMonPredAt. by unseal. Qed.
+Global Instance make_monPred_at_in i j : MakeMonPredAt j (monPred_in i) âŒœi âŠ‘ jâŒ.
+Proof. rewrite /MakeMonPredAt. by unseal. Qed.
+Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
+Proof. by rewrite /MakeMonPredAt. Qed.
 
-Global Instance from_assumption_make_monPred_car_l p i j P ð“Ÿ :
-  MakeMonPredCar i P ð“Ÿ â†’ IsBiIndexRel j i â†’ FromAssumption p (P j) ð“Ÿ.
+Global Instance from_assumption_make_monPred_at_l p i j P ð“Ÿ :
+  MakeMonPredAt i P ð“Ÿ â†’ IsBiIndexRel j i â†’ FromAssumption p (P j) ð“Ÿ.
 Proof.
-  rewrite /MakeMonPredCar /FromAssumption /IsBiIndexRel=><- ->.
+  rewrite /MakeMonPredAt /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).
+Global Instance from_assumption_make_monPred_at_r p i j P ð“Ÿ :
+  MakeMonPredAt i P ð“Ÿ â†’ IsBiIndexRel i j â†’ FromAssumption p ð“Ÿ (P j).
 Proof.
-  rewrite /MakeMonPredCar /FromAssumption /IsBiIndexRel=><- ->.
+  rewrite /MakeMonPredAt /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.
+Global Instance as_valid_monPred_at Ï† P (Î¦ : I â†’ PROP) :
+  AsValid Ï† P â†’ (âˆ€ i, MakeMonPredAt i P (Î¦ i)) â†’ AsValid' Ï† (âˆ€ i, Î¦ i) | 100.
 Proof.
-  rewrite /MakeMonPredCar /AsValid' /AsValid /bi_valid=> -> EQ.
+  rewrite /MakeMonPredAt /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) :
+Global Instance as_valid_monPred_at_wand Ï† P Q (Î¦ Î¨ : I â†’ PROP) :
   AsValid Ï† (P -âˆ— Q) â†’
-  (âˆ€ i, MakeMonPredCar i P (Î¦ i)) â†’ (âˆ€ i, MakeMonPredCar i Q (Î¨ i)) â†’
+  (âˆ€ i, MakeMonPredAt i P (Î¦ i)) â†’ (âˆ€ i, MakeMonPredAt i Q (Î¨ i)) â†’
   AsValid' Ï† (âˆ€ i, Î¦ i -âˆ— Î¨ i).
 Proof.
-  rewrite /AsValid' /AsValid /MakeMonPredCar. intros -> EQ1 EQ2.
+  rewrite /AsValid' /AsValid /MakeMonPredAt. 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) :
+Global Instance as_valid_monPred_at_equiv Ï† P Q (Î¦ Î¨ : I â†’ PROP) :
   AsValid Ï† (P âˆ—-âˆ— Q) â†’
-  (âˆ€ i, MakeMonPredCar i P (Î¦ i)) â†’ (âˆ€ i, MakeMonPredCar i Q (Î¨ i)) â†’
+  (âˆ€ i, MakeMonPredAt i P (Î¦ i)) â†’ (âˆ€ i, MakeMonPredAt i Q (Î¨ i)) â†’
   AsValid' Ï† (âˆ€ i, Î¦ i âˆ—-âˆ— Î¨ i).
 Proof.
-  rewrite /AsValid' /AsValid /MakeMonPredCar. intros -> EQ1 EQ2.
+  rewrite /AsValid' /AsValid /MakeMonPredAt. 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 :
+Global Instance into_pure_monPred_at P Ï† i :
   IntoPure P Ï† â†’ IntoPure (P i) Ï†.
 Proof. rewrite /IntoPure=>->. by unseal. Qed.
-Global Instance from_pure_monPred_car P Ï† i :
+Global Instance from_pure_monPred_at P Ï† i :
   FromPure P Ï† â†’ FromPure (P i) Ï†.
 Proof. rewrite /FromPure=><-. by unseal. Qed.
 Global Instance into_pure_monPred_in i j :
@@ -128,53 +128,53 @@ 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 :
+Global Instance into_internal_eq_monPred_at {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.
+Global Instance into_persistent_monPred_at p P Q ð“  i :
+  IntoPersistent p P Q â†’ MakeMonPredAt i Q ð“  â†’ IntoPersistent p (P i) ð“  | 0.
 Proof.
-  rewrite /IntoPersistent /MakeMonPredCar /bi_persistently_if.
+  rewrite /IntoPersistent /MakeMonPredAt /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 ð“  â†’
+Global Instance from_always_monPred_at a pe P Q ð“  i :
+  FromAlways a pe false P Q â†’ MakeMonPredAt i Q ð“  â†’
   FromAlways a pe false (P i) ð“  | 0.
 Proof.
-  rewrite /FromAlways /MakeMonPredCar /bi_persistently_if /bi_affinely_if=><-.
+  rewrite /FromAlways /MakeMonPredAt /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 ð“  â†’
+Lemma into_wand_monPred_at_unknown_unknown p q R P ð“Ÿ Q ð“  i :
+  IntoWand p q R P Q â†’  MakeMonPredAt i P ð“Ÿ â†’ MakeMonPredAt i Q ð“  â†’
   IntoWand p q (R i) ð“Ÿ ð“ .
 Proof.
-  rewrite /IntoWand /MakeMonPredCar /bi_affinely_if /bi_persistently_if.
+  rewrite /IntoWand /MakeMonPredAt /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 :
+Lemma into_wand_monPred_at_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).
+  MakeMonPredAt j P ð“Ÿ â†’ IntoWand p q (R i) ð“Ÿ (Q j).
 Proof.
-  rewrite /IntoWand /IsBiIndexRel /MakeMonPredCar=>-> ? ?.
-  eapply into_wand_monPred_car_unknown_unknown=>//. apply _.
+  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
+  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
 Qed.
-Lemma into_wand_monPred_car_known_unknown_le p q R P Q ð“  i j :
+Lemma into_wand_monPred_at_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) ð“ .
+  MakeMonPredAt j Q ð“  â†’ IntoWand p q (R i) (P j) ð“ .
 Proof.
-  rewrite /IntoWand /IsBiIndexRel /MakeMonPredCar=>-> ? ?.
-  eapply into_wand_monPred_car_unknown_unknown=>//. apply _.
+  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
+  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
 Qed.
-Lemma into_wand_monPred_car_known_unknown_ge p q R P Q ð“  i j :
+Lemma into_wand_monPred_at_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) ð“ .
+  MakeMonPredAt j Q ð“  â†’ IntoWand p q (R j) (P i) ð“ .
 Proof.
-  rewrite /IntoWand /IsBiIndexRel /MakeMonPredCar=>-> ? ?.
-  eapply into_wand_monPred_car_unknown_unknown=>//. apply _.
+  rewrite /IntoWand /IsBiIndexRel /MakeMonPredAt=>-> ? ?.
+  eapply into_wand_monPred_at_unknown_unknown=>//. apply _.
 Qed.
 
 Global Instance into_wand_wand'_monPred p q P Q ð“Ÿ ð“  i :
@@ -184,143 +184,143 @@ 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)) â†’
+Global Instance from_forall_monPred_at_wand P Q (Î¦ Î¨ : I â†’ PROP) i :
+  (âˆ€ j, MakeMonPredAt j P (Î¦ j)) â†’ (âˆ€ j, MakeMonPredAt 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.
+  rewrite /FromForall /MakeMonPredAt. 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)) â†’
+Global Instance from_forall_monPred_at_impl P Q (Î¦ Î¨ : I â†’ PROP) i :
+  (âˆ€ j, MakeMonPredAt j P (Î¦ j)) â†’ (âˆ€ j, MakeMonPredAt 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.
+  rewrite /FromForall /MakeMonPredAt. 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 :
+Global Instance into_forall_monPred_at_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 â†’
+Global Instance from_and_monPred_at P Q1 ð“ 1 Q2 ð“ 2 i :
+  FromAnd P Q1 Q2 â†’ MakeMonPredAt i Q1 ð“ 1 â†’ MakeMonPredAt 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 â†’
+Proof. rewrite /FromAnd /MakeMonPredAt /MakeMonPredAt=> <- <- <-. by unseal. Qed.
+Global Instance into_and_monPred_at p P Q1 ð“ 1 Q2 ð“ 2 i :
+  IntoAnd p P Q1 Q2 â†’ MakeMonPredAt i Q1 ð“ 1 â†’ MakeMonPredAt i Q2 ð“ 2 â†’
   IntoAnd p (P i) ð“ 1 ð“ 2.
 Proof.
-  rewrite /IntoAnd /MakeMonPredCar /bi_affinely_if /bi_persistently_if.
+  rewrite /IntoAnd /MakeMonPredAt /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 â†’
+Global Instance from_sep_monPred_at P Q1 ð“ 1 Q2 ð“ 2 i :
+  FromSep P Q1 Q2 â†’ MakeMonPredAt i Q1 ð“ 1 â†’ MakeMonPredAt 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 â†’
+Proof. rewrite /FromSep /MakeMonPredAt=> <- <- <-. by unseal. Qed.
+Global Instance into_sep_monPred_at P Q1 ð“ 1 Q2 ð“ 2 i :
+  IntoSep P Q1 Q2 â†’ MakeMonPredAt i Q1 ð“ 1 â†’ MakeMonPredAt i Q2 ð“ 2 â†’
   IntoSep (P i) ð“ 1 ð“ 2.
-Proof. rewrite /IntoSep /MakeMonPredCar=> -> <- <-. by unseal. Qed.
+Proof. rewrite /IntoSep /MakeMonPredAt=> -> <- <-. 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 â†’
+Global Instance from_or_monPred_at P Q1 ð“ 1 Q2 ð“ 2 i :
+  FromOr P Q1 Q2 â†’ MakeMonPredAt i Q1 ð“ 1 â†’ MakeMonPredAt 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 â†’
+Proof. rewrite /FromOr /MakeMonPredAt=> <- <- <-. by unseal. Qed.
+Global Instance into_or_monPred_at P Q1 ð“ 1 Q2 ð“ 2 i :
+  IntoOr P Q1 Q2 â†’ MakeMonPredAt i Q1 ð“ 1 â†’ MakeMonPredAt i Q2 ð“ 2 â†’
   IntoOr (P i) ð“ 1 ð“ 2.
-Proof. rewrite /IntoOr /MakeMonPredCar=> -> <- <-. by unseal. Qed.
+Proof. rewrite /IntoOr /MakeMonPredAt=> -> <- <-. 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) Î¨.
+Global Instance from_exist_monPred_at {A} P (Î¦ : A â†’ monPred) (Î¨ : A â†’ PROP) i :
+  FromExist P Î¦ â†’ (âˆ€ a, MakeMonPredAt i (Î¦ a) (Î¨ a)) â†’ FromExist (P i) Î¨.
 Proof.
-  rewrite /FromExist /MakeMonPredCar=><- H. setoid_rewrite <- H. by unseal.
+  rewrite /FromExist /MakeMonPredAt=><- 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) Î¨.
+Global Instance into_exist_monPred_at {A} P (Î¦ : A â†’ monPred) (Î¨ : A â†’ PROP) i :
+  IntoExist P Î¦ â†’ (âˆ€ a, MakeMonPredAt i (Î¦ a) (Î¨ a)) â†’ IntoExist (P i) Î¨.
 Proof.
-  rewrite /IntoExist /MakeMonPredCar=>-> H. setoid_rewrite <- H. by unseal.
+  rewrite /IntoExist /MakeMonPredAt=>-> H. setoid_rewrite <- H. by unseal.
 Qed.
 
-Global Instance foram_forall_monPred_car_plainly i P Î¦ :
-  (âˆ€ i, MakeMonPredCar i P (Î¦ i)) â†’
+Global Instance foram_forall_monPred_at_plainly i P Î¦ :
+  (âˆ€ i, MakeMonPredAt 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)) â†’
+Proof. rewrite /FromForall /MakeMonPredAt=>H. unseal. do 3 f_equiv. rewrite H //. Qed.
+Global Instance into_forall_monPred_at_plainly i P Î¦ :
+  (âˆ€ i, MakeMonPredAt 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.
+Proof. rewrite /IntoForall /MakeMonPredAt=>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) Î¦.
+Global Instance from_forall_monPred_at_all P (Î¦ : I â†’ PROP) i :
+  (âˆ€ i, MakeMonPredAt i P (Î¦ i)) â†’ FromForall (monPred_all P i) Î¦.
 Proof.
-  rewrite /FromForall /MakeMonPredCar=>H. setoid_rewrite <- H. by unseal.
+  rewrite /FromForall /MakeMonPredAt=>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) Î¦.
+Global Instance into_forall_monPred_at_all P (Î¦ : I â†’ PROP) i :
+  (âˆ€ i, MakeMonPredAt i P (Î¦ i)) â†’ IntoForall (monPred_all P i) Î¦.
 Proof.
-  rewrite /IntoForall /MakeMonPredCar=>H. setoid_rewrite <- H. by unseal.
+  rewrite /IntoForall /MakeMonPredAt=>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) Î¨.
+Global Instance from_forall_monPred_at {A} P (Î¦ : A â†’ monPred) (Î¨ : A â†’ PROP) i :
+  FromForall P Î¦ â†’ (âˆ€ a, MakeMonPredAt i (Î¦ a) (Î¨ a)) â†’ FromForall (P i) Î¨.
 Proof.
-  rewrite /FromForall /MakeMonPredCar=><- H. setoid_rewrite <- H. by unseal.
+  rewrite /FromForall /MakeMonPredAt=><- 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) Î¨.
+Global Instance into_forall_monPred_at {A} P (Î¦ : A â†’ monPred) (Î¨ : A â†’ PROP) i :
+  IntoForall P Î¦ â†’ (âˆ€ a, MakeMonPredAt i (Î¦ a) (Î¨ a)) â†’ IntoForall (P i) Î¨.
 Proof.
-  rewrite /IntoForall /MakeMonPredCar=>-> H. setoid_rewrite <- H. by unseal.
+  rewrite /IntoForall /MakeMonPredAt=>-> 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
+   monPred_at. 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 ð“  â†’
+Global Instance frame_monPred_at p P Q ð“  R i j :
+  IsBiIndexRel i j â†’ Frame p R P Q â†’ MakeMonPredAt j Q ð“  â†’
   Frame p (R i) (P j) ð“ .
 Proof.
-  rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if
+  rewrite /Frame /MakeMonPredAt /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) ð“ .
+Global Instance frame_monPred_at_embed i p P Q ð“  ð“¡ :
+  Frame p âŽ¡ð“¡âŽ¤ P Q â†’ MakeMonPredAt i Q ð“  â†’ Frame p ð“¡ (P i) ð“ .
 Proof.
-  rewrite /Frame /MakeMonPredCar /bi_affinely_if /bi_persistently_if=> <- <-.
+  rewrite /Frame /MakeMonPredAt /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.
+Global Instance from_modal_monPred_at i P Q ð“  :
+  FromModal P Q â†’ MakeMonPredAt i Q ð“  â†’ FromModal (P i) ð“ .
+Proof. by rewrite /FromModal /MakeMonPredAt=> <- <-. 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
+   (R i) P Q], we use [MakeMonPredAt] 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].
+   do not want to use [MakeMonPredAt].
 
    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) =>
+   version of [into_wand_monPred_at_xx_xx]. *)
+Hint Extern 3 (IntoWand _ _ (monPred_at _ _) ?P ?Q) =>
      is_evar P; is_evar Q;
-     eapply @into_wand_monPred_car_unknown_unknown
+     eapply @into_wand_monPred_at_unknown_unknown
      : typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_car _ _) ?P (monPred_car ?Q _)) =>
-     eapply @into_wand_monPred_car_unknown_known
+Hint Extern 2 (IntoWand _ _ (monPred_at _ _) ?P (monPred_at ?Q _)) =>
+     eapply @into_wand_monPred_at_unknown_known
      : typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_car _ _) (monPred_car ?P _) ?Q) =>
-     eapply @into_wand_monPred_car_known_unknown_le
+Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
+     eapply @into_wand_monPred_at_known_unknown_le
      : typeclass_instances.
-Hint Extern 2 (IntoWand _ _ (monPred_car _ _) (monPred_car ?P _) ?Q) =>
-     eapply @into_wand_monPred_car_known_unknown_ge
+Hint Extern 2 (IntoWand _ _ (monPred_at _ _) (monPred_at ?P _) ?Q) =>
+     eapply @into_wand_monPred_at_known_unknown_ge
      : typeclass_instances.
 
 Section sbi.
@@ -331,33 +331,33 @@ Implicit Types ð“Ÿ ð“  ð“¡ : PROP.
 Implicit Types Ï† : Prop.
 Implicit Types i j : I.
 
-Global Instance is_except_0_monPred_car i P :
+Global Instance is_except_0_monPred_at 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 make_monPred_at_except_0 i P ð“  :
+  MakeMonPredAt i P ð“  â†’ MakeMonPredAt i (â—‡ P)%I (â—‡ ð“ )%I.
+Proof. rewrite /MakeMonPredAt=><-. by unseal. Qed.
+Global Instance make_monPred_at_later i P ð“  :
+  MakeMonPredAt i P ð“  â†’ MakeMonPredAt i (â–· P)%I (â–· ð“ )%I.
+Proof. rewrite /MakeMonPredAt=><-. by unseal. Qed.
+Global Instance make_monPred_at_laterN i n P ð“  :
+  MakeMonPredAt i P ð“  â†’ MakeMonPredAt i (â–·^n P)%I (â–·^n ð“ )%I.
+Proof. rewrite /MakeMonPredAt=> <-. 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_except_0_monPred_at_fwd i P Q ð“  :
+  IntoExcept0 P Q â†’ MakeMonPredAt i Q ð“  â†’ IntoExcept0 (P i) ð“ .
+Proof. rewrite /IntoExcept0 /MakeMonPredAt=> -> <-. by unseal. Qed.
+Global Instance into_except_0_monPred_at_bwd i P ð“Ÿ Q :
+  IntoExcept0 P Q â†’ MakeMonPredAt i P ð“Ÿ â†’ IntoExcept0 ð“Ÿ (Q i).
+Proof. rewrite /IntoExcept0 /MakeMonPredAt=> 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) ð“ .
+Global Instance into_later_monPred_at i n P Q ð“  :
+  IntoLaterN n P Q â†’ MakeMonPredAt i Q ð“  â†’ IntoLaterN n (P i) ð“ .
 Proof.
-  rewrite /IntoLaterN /MakeMonPredCar=> -> <-. elim n=>//= ? <-. by unseal.
+  rewrite /IntoLaterN /MakeMonPredAt=> -> <-. 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.
+Global Instance from_later_monPred_at i n P Q ð“  :
+  FromLaterN n P Q â†’ MakeMonPredAt i Q ð“  â†’ FromLaterN n (P i) ð“ .
+Proof. rewrite /FromLaterN /MakeMonPredAt=> <- <-. elim n=>//= ? ->. by unseal. Qed.
 End sbi.