diff --git a/ProofMode.md b/ProofMode.md
index acc6d86defda6fd245e5da7953f4f36d543ad85f..0143260d08d0858e433d9a8b3cd3da3b88ee0a33 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -117,7 +117,7 @@ Modalities
 - `iModIntro mod` : introduction of a modality. The type class `FromModal` is
   used to specify which modalities this tactic should introduce. Instances of
   that type class include: later, except 0, basic update and fancy update,
-  persistently, affinely, plainly, absorbingly, absolutely, and relatively.
+  persistently, affinely, plainly, absorbingly, objectively, and subjectively.
   The optional argument `mod` can be used to specify what modality to introduce
   in case of ambiguity, e.g. `⎡|==> P⎤`.
 - `iAlways` : a deprecated alias of `iModIntro`.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index c126c39334338cf2e5834754ecaeb6bbb9851d17..2bbd331ba48d4272da5392c2bd062c2b963ca9b1 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -16,8 +16,7 @@ Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
 (* Own and valid derived *)
-Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
-  ✓ a ⊢ bi_persistently (✓ a : uPred M).
+Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
 Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
 Lemma affinely_persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 4284299a89ec8ed6fa7d35fbd43edf706e338f1e..deb0ec4bb45d71b53aef1950a40151fbf50765f1 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -457,21 +457,21 @@ Proof.
   - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
     intros P Q R. unseal=> HPQR. split; intros n x ? (?&?&?&?&?). ofe_subst.
     eapply HPQR; eauto using cmra_validN_op_l.
-  - (* (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q *)
+  - (* (P ⊢ Q) → <pers> P ⊢ <pers> Q *)
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, cmra_core_validN.
-  - (* bi_persistently P ⊢ bi_persistently (bi_persistently P) *)
+  - (* <pers> P ⊢ <pers> <pers> P *)
     intros P. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp.
-  - (* P ⊢ bi_persistently emp (ADMISSIBLE) *)
+  - (* P ⊢ <pers> emp (ADMISSIBLE) *)
     by unseal.
-  - (* (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a) *)
+  - (* (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a) *)
     by unseal.
-  - (* bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a) *)
+  - (* <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a) *)
     by unseal.
-  - (* bi_persistently P ∗ Q ⊢ bi_persistently P (ADMISSIBLE) *)
+  - (* <pers> P ∗ Q ⊢ <pers> P (ADMISSIBLE) *)
     intros P Q. move: (uPred_persistently P)=> P'.
     unseal; split; intros n x ? (x1&x2&?&?&_); ofe_subst;
       eauto using uPred_mono, cmra_includedN_l.
-  - (* bi_persistently P ∧ Q ⊢ P ∗ Q *)
+  - (* <pers> P ∧ Q ⊢ P ∗ Q *)
     intros P Q. unseal; split=> n x ? [??]; simpl in *.
     exists (core x), x; rewrite ?cmra_core_l; auto.
 Qed.
@@ -523,9 +523,9 @@ Proof.
   - (* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
     intros P Q. unseal; split=> -[|n] x ? /=; [done|intros (x1&x2&Hx&?&?)].
     exists x1, x2; eauto using dist_S.
-  - (* ▷ bi_persistently P ⊢ bi_persistently (▷ P) *)
+  - (* ▷ <pers> P ⊢ <pers> ▷ P *)
     by unseal.
-  - (* bi_persistently (▷ P) ⊢ ▷ bi_persistently P *)
+  - (* <pers> ▷ P ⊢ ▷ <pers> P *)
     by unseal.
   - (* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
     intros P. unseal; split=> -[|n] x ? /= HP; [by left|right].
@@ -552,13 +552,13 @@ Proof.
     unseal; split=> n' x; split; apply HP; eauto using @ucmra_unit_validN.
   - (* (P ⊢ Q) → ■ P ⊢ ■ Q *)
     intros P QR HP. unseal; split=> n x ? /=. by apply HP, ucmra_unit_validN.
-  - (* ■ P ⊢ bi_persistently P *)
+  - (* ■ P ⊢ <pers> P *)
     unseal; split; simpl; eauto using uPred_mono, @ucmra_unit_leastN.
   - (* ■ P ⊢ ■ ■ P *)
     unseal; split=> n x ?? //.
   - (* (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a) *)
     by unseal.
-  - (* (■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q) *)
+  - (* (■ P → <pers> Q) ⊢ <pers> (■ P → Q) *)
     unseal; split=> /= n x ? HPQ n' x' ????.
     eapply uPred_mono with n' (core x)=>//; [|by apply cmra_included_includedN].
     apply (HPQ n' x); eauto using cmra_validN_le.
@@ -665,8 +665,7 @@ Proof.
     by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
       -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
 Qed.
-Lemma persistently_ownM_core (a : M) :
-  uPred_ownM a ⊢ bi_persistently (uPred_ownM (core a)).
+Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
 Proof.
   rewrite /bi_persistently /=. unseal.
   split=> n x Hx /=. by apply cmra_core_monoN.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index d7648e9287febcd3da580f7b3a9af2a9703d6aa8..a51063fdc1797bc3d32f760e4fe39a2c17eea444 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -127,8 +127,7 @@ Section sep_list.
   Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
-    bi_persistently ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢
-    [∗ list] k↦x ∈ l, bi_persistently (Φ k x).
+    <pers> ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ [∗ list] k↦x ∈ l, <pers> (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_sepL_forall `{BiAffine PROP} Φ l :
@@ -266,8 +265,7 @@ Section and_list.
   Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_andL_persistently Φ l :
-    bi_persistently ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢
-    [∧ list] k↦x ∈ l, bi_persistently (Φ k x).
+    <pers> ([∧ list] k↦x ∈ l, Φ k x) ⊣⊢ [∧ list] k↦x ∈ l, <pers> (Φ k x).
   Proof. apply (big_opL_commute _). Qed.
 
   Lemma big_andL_forall `{BiAffine PROP} Φ l :
@@ -398,8 +396,7 @@ Section gmap.
   Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
-    (bi_persistently ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢
-      ([∗ map] k↦x ∈ m, bi_persistently (Φ k x)).
+    (<pers> ([∗ map] k↦x ∈ m, Φ k x)) ⊣⊢ ([∗ map] k↦x ∈ m, <pers> (Φ k x)).
   Proof. apply (big_opM_commute _). Qed.
 
   Lemma big_sepM_forall `{BiAffine PROP} Φ m :
@@ -564,7 +561,7 @@ Section gset.
   Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
-    bi_persistently ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, bi_persistently (Φ y).
+    <pers> ([∗ set] y ∈ X, Φ y) ⊣⊢ [∗ set] y ∈ X, <pers> (Φ y).
   Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_forall `{BiAffine PROP} Φ X :
@@ -672,8 +669,7 @@ Section gmultiset.
   Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
 
   Lemma big_sepMS_persistently `{BiAffine PROP} Φ X :
-    bi_persistently ([∗ mset] y ∈ X, Φ y) ⊣⊢
-      [∗ mset] y ∈ X, bi_persistently (Φ y).
+    <pers> ([∗ mset] y ∈ X, Φ y) ⊣⊢ [∗ mset] y ∈ X, <pers> (Φ y).
   Proof. apply (big_opMS_commute _). Qed.
 
   Global Instance big_sepMS_empty_persistent Φ :
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index b687a3d4c362d48757323ab66b8f2e37fd665b98..a381402bf87147a637ac2623cc77162bda5a2048 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -13,7 +13,7 @@ Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Instance: Params (@bi_wand_iff) 1.
 Infix "∗-∗" := bi_wand_iff (at level 95, no associativity) : bi_scope.
 
-Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ bi_persistently P.
+Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
 Arguments Persistent {_} _%I : simpl never.
 Arguments persistent {_} _%I {_}.
 Hint Mode Persistent + ! : typeclass_instances.
@@ -23,7 +23,10 @@ Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
 Arguments bi_affinely {_} _%I : simpl never.
 Instance: Params (@bi_affinely) 1.
 Typeclasses Opaque bi_affinely.
-Notation "â–¡ P" := (bi_affinely (bi_persistently P))%I
+Notation "'<affine>' P" := (bi_affinely P)
+  (at level 20, right associativity) : bi_scope.
+
+Notation "â–¡ P" := (<affine> <pers> P)%I
   (at level 20, right associativity) : bi_scope.
 
 Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
@@ -36,31 +39,40 @@ Hint Mode BiAffine ! : typeclass_instances.
 Existing Instance absorbing_bi | 0.
 
 Class BiPositive (PROP : bi) :=
-  bi_positive (P Q : PROP) : bi_affinely (P ∗ Q) ⊢ bi_affinely P ∗ Q.
+  bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
 Hint Mode BiPositive ! : typeclass_instances.
 
 Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
 Arguments bi_absorbingly {_} _%I : simpl never.
 Instance: Params (@bi_absorbingly) 1.
 Typeclasses Opaque bi_absorbingly.
+Notation "'<absorb>' P" := (bi_absorbingly P)
+  (at level 20, right associativity) : bi_scope.
 
-Class Absorbing {PROP : bi} (P : PROP) := absorbing : bi_absorbingly P ⊢ P.
+Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
 Arguments Absorbing {_} _%I : simpl never.
 Arguments absorbing {_} _%I.
 Hint Mode Absorbing + ! : typeclass_instances.
 
 Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then bi_persistently P else P)%I.
+  (if p then <pers> P else P)%I.
 Arguments bi_persistently_if {_} !_ _%I /.
 Instance: Params (@bi_persistently_if) 2.
 Typeclasses Opaque bi_persistently_if.
+Notation "'<pers>?' p P" := (bi_persistently_if p P)
+  (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<pers>?' p  P") : bi_scope.
 
 Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
-  (if p then bi_affinely P else P)%I.
+  (if p then <affine> P else P)%I.
 Arguments bi_affinely_if {_} !_ _%I /.
 Instance: Params (@bi_affinely_if) 2.
 Typeclasses Opaque bi_affinely_if.
-Notation "â–¡? p P" := (bi_affinely_if p (bi_persistently_if p P))%I
+Notation "'<affine>?' p P" := (bi_affinely_if p P)
+  (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<affine>?' p  P") : bi_scope.
+
+Notation "â–¡? p P" := (<affine>?p <pers>?p P)%I
   (at level 20, p at level 9, P at level 20,
    right associativity, format "â–¡? p  P") : bi_scope.
 
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 474bf1bb7c390a79eb113b99730bcf59f5746860..e55ac337d6fc3b003fb11aec7c9c36617d4253d3 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -506,56 +506,54 @@ Global Instance affinely_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely PROP).
 Proof. solve_proper. Qed.
 
-Lemma affinely_elim_emp P : bi_affinely P ⊢ emp.
+Lemma affinely_elim_emp P : <affine> P ⊢ emp.
 Proof. rewrite /bi_affinely; auto. Qed.
-Lemma affinely_elim P : bi_affinely P ⊢ P.
+Lemma affinely_elim P : <affine> P ⊢ P.
 Proof. rewrite /bi_affinely; auto. Qed.
-Lemma affinely_mono P Q : (P ⊢ Q) → bi_affinely P ⊢ bi_affinely Q.
+Lemma affinely_mono P Q : (P ⊢ Q) → <affine> P ⊢ <affine> Q.
 Proof. by intros ->. Qed.
-Lemma affinely_idemp P : bi_affinely (bi_affinely P) ⊣⊢ bi_affinely P.
+Lemma affinely_idemp P : <affine> <affine> P ⊣⊢ <affine> P.
 Proof. by rewrite /bi_affinely assoc idemp. Qed.
 
-Lemma affinely_intro' P Q : (bi_affinely P ⊢ Q) → bi_affinely P ⊢ bi_affinely Q.
+Lemma affinely_intro' P Q : (<affine> P ⊢ Q) → <affine> P ⊢ <affine> Q.
 Proof. intros <-. by rewrite affinely_idemp. Qed.
 
-Lemma affinely_False : bi_affinely False ⊣⊢ False.
+Lemma affinely_False : <affine> False ⊣⊢ False.
 Proof. by rewrite /bi_affinely right_absorb. Qed.
-Lemma affinely_emp : bi_affinely emp ⊣⊢ emp.
+Lemma affinely_emp : <affine> emp ⊣⊢ emp.
 Proof. by rewrite /bi_affinely (idemp bi_and). Qed.
-Lemma affinely_or P Q : bi_affinely (P ∨ Q) ⊣⊢ bi_affinely P ∨ bi_affinely Q.
+Lemma affinely_or P Q : <affine> (P ∨ Q) ⊣⊢ <affine> P ∨ <affine> Q.
 Proof. by rewrite /bi_affinely and_or_l. Qed.
-Lemma affinely_and P Q : bi_affinely (P ∧ Q) ⊣⊢ bi_affinely P ∧ bi_affinely Q.
+Lemma affinely_and P Q : <affine> (P ∧ Q) ⊣⊢ <affine> P ∧ <affine> Q.
 Proof.
   rewrite /bi_affinely -(comm _ P) (assoc _ (_ ∧ _)%I) -!(assoc _ P).
   by rewrite idemp !assoc (comm _ P).
 Qed.
-Lemma affinely_sep_2 P Q : bi_affinely P ∗ bi_affinely Q ⊢ bi_affinely (P ∗ Q).
+Lemma affinely_sep_2 P Q : <affine> P ∗ <affine> Q ⊢ <affine> (P ∗ Q).
 Proof.
   rewrite /bi_affinely. apply and_intro.
   - by rewrite !and_elim_l right_id.
   - by rewrite !and_elim_r.
 Qed.
 Lemma affinely_sep `{BiPositive PROP} P Q :
-  bi_affinely (P ∗ Q) ⊣⊢ bi_affinely P ∗ bi_affinely Q.
+  <affine> (P ∗ Q) ⊣⊢ <affine> P ∗ <affine> Q.
 Proof.
   apply (anti_symm _), affinely_sep_2.
-  by rewrite -{1}affinely_idemp bi_positive !(comm _ (bi_affinely P)%I) bi_positive.
+  by rewrite -{1}affinely_idemp bi_positive !(comm _ (<affine> P)%I) bi_positive.
 Qed.
-Lemma affinely_forall {A} (Φ : A → PROP) :
-  bi_affinely (∀ a, Φ a) ⊢ ∀ a, bi_affinely (Φ a).
+Lemma affinely_forall {A} (Φ : A → PROP) : <affine> (∀ a, Φ a) ⊢ ∀ a, <affine> (Φ a).
 Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
-Lemma affinely_exist {A} (Φ : A → PROP) :
-  bi_affinely (∃ a, Φ a) ⊣⊢ ∃ a, bi_affinely (Φ a).
+Lemma affinely_exist {A} (Φ : A → PROP) : <affine> (∃ a, Φ a) ⊣⊢ ∃ a, <affine> (Φ a).
 Proof. by rewrite /bi_affinely and_exist_l. Qed.
 
-Lemma affinely_True_emp : bi_affinely True ⊣⊢ bi_affinely emp.
+Lemma affinely_True_emp : <affine> True ⊣⊢ <affine> emp.
 Proof. apply (anti_symm _); rewrite /bi_affinely; auto. Qed.
 
-Lemma affinely_and_l P Q : bi_affinely P ∧ Q ⊣⊢ bi_affinely (P ∧ Q).
+Lemma affinely_and_l P Q : <affine> P ∧ Q ⊣⊢ <affine> (P ∧ Q).
 Proof. by rewrite /bi_affinely assoc. Qed.
-Lemma affinely_and_r P Q : P ∧ bi_affinely Q ⊣⊢ bi_affinely (P ∧ Q).
+Lemma affinely_and_r P Q : P ∧ <affine> Q ⊣⊢ <affine> (P ∧ Q).
 Proof. by rewrite /bi_affinely !assoc (comm _ P). Qed.
-Lemma affinely_and_lr P Q : bi_affinely P ∧ Q ⊣⊢ P ∧ bi_affinely Q.
+Lemma affinely_and_lr P Q : <affine> P ∧ Q ⊣⊢ P ∧ <affine> Q.
 Proof. by rewrite affinely_and_l affinely_and_r. Qed.
 
 (* Properties of the absorbingly modality *)
@@ -569,50 +567,45 @@ Global Instance absorbingly_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_absorbingly PROP).
 Proof. solve_proper. Qed.
 
-Lemma absorbingly_intro P : P ⊢ bi_absorbingly P.
+Lemma absorbingly_intro P : P ⊢ <absorb> P.
 Proof. by rewrite /bi_absorbingly -True_sep_2. Qed.
-Lemma absorbingly_mono P Q : (P ⊢ Q) → bi_absorbingly P ⊢ bi_absorbingly Q.
+Lemma absorbingly_mono P Q : (P ⊢ Q) → <absorb> P ⊢ <absorb> Q.
 Proof. by intros ->. Qed.
-Lemma absorbingly_idemp P : bi_absorbingly (bi_absorbingly P) ⊣⊢ bi_absorbingly P.
+Lemma absorbingly_idemp P : <absorb> <absorb> P ⊣⊢ <absorb> P.
 Proof.
   apply (anti_symm _), absorbingly_intro.
   rewrite /bi_absorbingly assoc. apply sep_mono; auto.
 Qed.
 
-Lemma absorbingly_pure φ : bi_absorbingly ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝.
+Lemma absorbingly_pure φ : <absorb> ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝.
 Proof.
   apply (anti_symm _), absorbingly_intro.
   apply wand_elim_r', pure_elim'=> ?. apply wand_intro_l; auto.
 Qed.
-Lemma absorbingly_or P Q :
-  bi_absorbingly (P ∨ Q) ⊣⊢ bi_absorbingly P ∨ bi_absorbingly Q.
+Lemma absorbingly_or P Q : <absorb> (P ∨ Q) ⊣⊢ <absorb> P ∨ <absorb> Q.
 Proof. by rewrite /bi_absorbingly sep_or_l. Qed.
-Lemma absorbingly_and P Q :
-  bi_absorbingly (P ∧ Q) ⊢ bi_absorbingly P ∧ bi_absorbingly Q.
+Lemma absorbingly_and P Q : <absorb> (P ∧ Q) ⊢ <absorb> P ∧ <absorb> Q.
 Proof. apply and_intro; apply absorbingly_mono; auto. Qed.
-Lemma absorbingly_forall {A} (Φ : A → PROP) :
-  bi_absorbingly (∀ a, Φ a) ⊢ ∀ a, bi_absorbingly (Φ a).
+Lemma absorbingly_forall {A} (Φ : A → PROP) : <absorb> (∀ a, Φ a) ⊢ ∀ a, <absorb> (Φ a).
 Proof. apply forall_intro=> a. by rewrite (forall_elim a). Qed.
-Lemma absorbingly_exist {A} (Φ : A → PROP) :
-  bi_absorbingly (∃ a, Φ a) ⊣⊢ ∃ a, bi_absorbingly (Φ a).
+Lemma absorbingly_exist {A} (Φ : A → PROP) : <absorb> (∃ a, Φ a) ⊣⊢ ∃ a, <absorb> (Φ a).
 Proof. by rewrite /bi_absorbingly sep_exist_l. Qed.
 
-Lemma absorbingly_sep P Q : bi_absorbingly (P ∗ Q) ⊣⊢ bi_absorbingly P ∗ bi_absorbingly Q.
+Lemma absorbingly_sep P Q : <absorb> (P ∗ Q) ⊣⊢ <absorb> P ∗ <absorb> Q.
 Proof. by rewrite -{1}absorbingly_idemp /bi_absorbingly !assoc -!(comm _ P) !assoc. Qed.
-Lemma absorbingly_True_emp : bi_absorbingly True ⊣⊢ bi_absorbingly emp.
+Lemma absorbingly_True_emp : <absorb> True ⊣⊢ <absorb> emp.
 Proof. by rewrite absorbingly_pure /bi_absorbingly right_id. Qed.
-Lemma absorbingly_wand P Q : bi_absorbingly (P -∗ Q) ⊢ bi_absorbingly P -∗ bi_absorbingly Q.
+Lemma absorbingly_wand P Q : <absorb> (P -∗ Q) ⊢ <absorb> P -∗ <absorb> Q.
 Proof. apply wand_intro_l. by rewrite -absorbingly_sep wand_elim_r. Qed.
 
-Lemma absorbingly_sep_l P Q : bi_absorbingly P ∗ Q ⊣⊢ bi_absorbingly (P ∗ Q).
+Lemma absorbingly_sep_l P Q : <absorb> P ∗ Q ⊣⊢ <absorb> (P ∗ Q).
 Proof. by rewrite /bi_absorbingly assoc. Qed.
-Lemma absorbingly_sep_r P Q : P ∗ bi_absorbingly Q ⊣⊢ bi_absorbingly (P ∗ Q).
+Lemma absorbingly_sep_r P Q : P ∗ <absorb> Q ⊣⊢ <absorb> (P ∗ Q).
 Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
-Lemma absorbingly_sep_lr P Q : bi_absorbingly P ∗ Q ⊣⊢ P ∗ bi_absorbingly Q.
+Lemma absorbingly_sep_lr P Q : <absorb> P ∗ Q ⊣⊢ P ∗ <absorb> Q.
 Proof. by rewrite absorbingly_sep_l absorbingly_sep_r. Qed.
 
-Lemma affinely_absorbingly `{!BiPositive PROP} P :
-  bi_affinely (bi_absorbingly P) ⊣⊢ bi_affinely P.
+Lemma affinely_absorbingly `{!BiPositive PROP} P : <affine> <absorb> P ⊣⊢ <affine> P.
 Proof.
   apply (anti_symm _), affinely_mono, absorbingly_intro.
   by rewrite /bi_absorbingly affinely_sep affinely_True_emp affinely_emp left_id.
@@ -624,9 +617,9 @@ Proof. solve_proper. Qed.
 Global Instance Absorbing_proper : Proper ((⊣⊢) ==> iff) (@Absorbing PROP).
 Proof. solve_proper. Qed.
 
-Lemma affine_affinely P `{!Affine P} : bi_affinely P ⊣⊢ P.
+Lemma affine_affinely P `{!Affine P} : <affine> P ⊣⊢ P.
 Proof. rewrite /bi_affinely. apply (anti_symm _); auto. Qed.
-Lemma absorbing_absorbingly P `{!Absorbing P} : bi_absorbingly P ⊣⊢ P.
+Lemma absorbing_absorbingly P `{!Absorbing P} : <absorb> P ⊣⊢ P.
 Proof. by apply (anti_symm _), absorbingly_intro. Qed.
 
 Lemma True_affine_all_affine P : Affine (True%I : PROP) → Affine P.
@@ -654,7 +647,7 @@ Proof.
     apply and_intro; apply: sep_elim_l || apply: sep_elim_r.
 Qed.
 
-Lemma affinely_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ bi_affinely Q.
+Lemma affinely_intro P Q `{!Affine P} : (P ⊢ Q) → P ⊢ <affine> Q.
 Proof. intros <-. by rewrite affine_affinely. Qed.
 
 Lemma emp_and P `{!Affine P} : emp ∧ P ⊣⊢ P.
@@ -721,58 +714,51 @@ Global Instance persistently_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently PROP).
 Proof. intros P Q; apply persistently_mono. Qed.
 
-Lemma absorbingly_persistently P :
-  bi_absorbingly (bi_persistently P) ⊣⊢ bi_persistently P.
+Lemma absorbingly_persistently P : <absorb> <pers> P ⊣⊢ <pers> P.
 Proof.
   apply (anti_symm _), absorbingly_intro.
   by rewrite /bi_absorbingly comm persistently_absorbing.
 Qed.
 
 Lemma persistently_forall {A} (Ψ : A → PROP) :
-  bi_persistently (∀ a, Ψ a) ⊣⊢ ∀ a, bi_persistently (Ψ a).
+  <pers> (∀ a, Ψ a) ⊣⊢ ∀ a, <pers> (Ψ a).
 Proof.
   apply (anti_symm _); auto using persistently_forall_2.
   apply forall_intro=> x. by rewrite (forall_elim x).
 Qed.
 Lemma persistently_exist {A} (Ψ : A → PROP) :
-  bi_persistently (∃ a, Ψ a) ⊣⊢ ∃ a, bi_persistently (Ψ a).
+  <pers> (∃ a, Ψ a) ⊣⊢ ∃ a, <pers> (Ψ a).
 Proof.
   apply (anti_symm _); auto using persistently_exist_1.
   apply exist_elim=> x. by rewrite (exist_intro x).
 Qed.
-Lemma persistently_and P Q :
-  bi_persistently (P ∧ Q) ⊣⊢ bi_persistently P ∧ bi_persistently Q.
+Lemma persistently_and P Q : <pers> (P ∧ Q) ⊣⊢ <pers> P ∧ <pers> Q.
 Proof. rewrite !and_alt persistently_forall. by apply forall_proper=> -[]. Qed.
-Lemma persistently_or P Q :
-  bi_persistently (P ∨ Q) ⊣⊢ bi_persistently P ∨ bi_persistently Q.
+Lemma persistently_or P Q : <pers> (P ∨ Q) ⊣⊢ <pers> P ∨ <pers> Q.
 Proof. rewrite !or_alt persistently_exist. by apply exist_proper=> -[]. Qed.
-Lemma persistently_impl P Q :
-  bi_persistently (P → Q) ⊢ bi_persistently P → bi_persistently Q.
+Lemma persistently_impl P Q : <pers> (P → Q) ⊢ <pers> P → <pers> Q.
 Proof.
   apply impl_intro_l; rewrite -persistently_and.
   apply persistently_mono, impl_elim with P; auto.
 Qed.
 
-Lemma persistently_True_emp : bi_persistently True ⊣⊢ bi_persistently emp.
+Lemma persistently_True_emp : <pers> True ⊣⊢ <pers> emp.
 Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
 
-Lemma persistently_and_emp P :
-  bi_persistently P ⊣⊢ bi_persistently (emp ∧ P).
+Lemma persistently_and_emp P : <pers> P ⊣⊢ <pers> (emp ∧ P).
 Proof.
   apply (anti_symm (⊢)); last by rewrite and_elim_r.
   rewrite persistently_and. apply and_intro; last done.
   apply persistently_emp_intro.
 Qed.
 
-Lemma persistently_and_sep_elim_emp P Q :
-  bi_persistently P ∧ Q ⊢ (emp ∧ P) ∗ Q.
+Lemma persistently_and_sep_elim_emp P Q : <pers> P ∧ Q ⊢ (emp ∧ P) ∗ Q.
 Proof.
   rewrite persistently_and_emp.
   apply persistently_and_sep_elim.
 Qed.
 
-Lemma persistently_and_sep_assoc P Q R :
-  bi_persistently P ∧ (Q ∗ R) ⊣⊢ (bi_persistently P ∧ Q) ∗ R.
+Lemma persistently_and_sep_assoc P Q R : <pers> P ∧ (Q ∗ R) ⊣⊢ (<pers> P ∧ Q) ∗ R.
 Proof.
   apply (anti_symm (⊢)).
   - rewrite {1}persistently_idemp_2 persistently_and_sep_elim_emp assoc.
@@ -783,79 +769,72 @@ Proof.
     + by rewrite and_elim_l persistently_absorbing.
     + by rewrite and_elim_r.
 Qed.
-Lemma persistently_and_emp_elim P : emp ∧ bi_persistently P ⊢ P.
+Lemma persistently_and_emp_elim P : emp ∧ <pers> P ⊢ P.
 Proof. by rewrite comm persistently_and_sep_elim_emp right_id and_elim_r. Qed.
-Lemma persistently_elim_absorbingly P : bi_persistently P ⊢ bi_absorbingly P.
+Lemma persistently_elim_absorbingly P : <pers> P ⊢ <absorb> P.
 Proof.
-  rewrite -(right_id True%I _ (bi_persistently _)%I) -{1}(left_id emp%I _ True%I).
+  rewrite -(right_id True%I _ (<pers> _)%I) -{1}(left_id emp%I _ True%I).
   by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim comm.
 Qed.
-Lemma persistently_elim P `{!Absorbing P} : bi_persistently P ⊢ P.
+Lemma persistently_elim P `{!Absorbing P} : <pers> P ⊢ P.
 Proof. by rewrite persistently_elim_absorbingly absorbing_absorbingly. Qed.
 
-Lemma persistently_idemp_1 P :
-  bi_persistently (bi_persistently P) ⊢ bi_persistently P.
+Lemma persistently_idemp_1 P : <pers> <pers> P ⊢ <pers> P.
 Proof. by rewrite persistently_elim_absorbingly absorbingly_persistently. Qed.
-Lemma persistently_idemp P :
-  bi_persistently (bi_persistently P) ⊣⊢ bi_persistently P.
+Lemma persistently_idemp P : <pers> <pers> P ⊣⊢ <pers> P.
 Proof. apply (anti_symm _); auto using persistently_idemp_1, persistently_idemp_2. Qed.
 
-Lemma persistently_intro' P Q :
-  (bi_persistently P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q.
+Lemma persistently_intro' P Q : (<pers> P ⊢ Q) → <pers> P ⊢ <pers> Q.
 Proof. intros <-. apply persistently_idemp_2. Qed.
 
-Lemma persistently_pure φ : bi_persistently ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Lemma persistently_pure φ : <pers> ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof.
   apply (anti_symm _).
   { by rewrite persistently_elim_absorbingly absorbingly_pure. }
   apply pure_elim'=> Hφ.
-  trans (∀ x : False, bi_persistently True : PROP)%I; [by apply forall_intro|].
+  trans (∀ x : False, <pers> True : PROP)%I; [by apply forall_intro|].
   rewrite persistently_forall_2. auto using persistently_mono, pure_intro.
 Qed.
 
-Lemma persistently_sep_dup P :
-  bi_persistently P ⊣⊢ bi_persistently P ∗ bi_persistently P.
+Lemma persistently_sep_dup P : <pers> P ⊣⊢ <pers> P ∗ <pers> P.
 Proof.
   apply (anti_symm _).
-  - rewrite -{1}(idemp bi_and (bi_persistently _)).
-    by rewrite -{2}(left_id emp%I _ (bi_persistently _))
+  - rewrite -{1}(idemp bi_and (<pers> _)%I).
+    by rewrite -{2}(left_id emp%I _ (<pers> _)%I)
       persistently_and_sep_assoc and_elim_l.
   - by rewrite persistently_absorbing.
 Qed.
 
-Lemma persistently_and_sep_l_1 P Q : bi_persistently P ∧ Q ⊢ bi_persistently P ∗ Q.
+Lemma persistently_and_sep_l_1 P Q : <pers> P ∧ Q ⊢ <pers> P ∗ Q.
 Proof.
   by rewrite -{1}(left_id emp%I _ Q%I) persistently_and_sep_assoc and_elim_l.
 Qed.
-Lemma persistently_and_sep_r_1 P Q : P ∧ bi_persistently Q ⊢ P ∗ bi_persistently Q.
+Lemma persistently_and_sep_r_1 P Q : P ∧ <pers> Q ⊢ P ∗ <pers> Q.
 Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
 
-Lemma persistently_and_sep P Q : bi_persistently (P ∧ Q) ⊢ bi_persistently (P ∗ Q).
+Lemma persistently_and_sep P Q : <pers> (P ∧ Q) ⊢ <pers> (P ∗ Q).
 Proof.
   rewrite persistently_and.
   rewrite -{1}persistently_idemp -persistently_and -{1}(left_id emp%I _ Q%I).
   by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
 Qed.
 
-Lemma persistently_affinely P : bi_persistently (bi_affinely P) ⊣⊢ bi_persistently P.
+Lemma persistently_affinely P : <pers> <affine> P ⊣⊢ <pers> P.
 Proof.
   by rewrite /bi_affinely persistently_and -persistently_True_emp
              persistently_pure left_id.
 Qed.
 
-Lemma and_sep_persistently P Q :
-  bi_persistently P ∧ bi_persistently Q ⊣⊢ bi_persistently P ∗ bi_persistently Q.
+Lemma and_sep_persistently P Q : <pers> P ∧ <pers> Q ⊣⊢ <pers> P ∗ <pers> Q.
 Proof.
   apply (anti_symm _); auto using persistently_and_sep_l_1.
   apply and_intro.
   - by rewrite persistently_absorbing.
   - by rewrite comm persistently_absorbing.
 Qed.
-Lemma persistently_sep_2 P Q :
-  bi_persistently P ∗ bi_persistently Q ⊢ bi_persistently (P ∗ Q).
+Lemma persistently_sep_2 P Q : <pers> P ∗ <pers> Q ⊢ <pers> (P ∗ Q).
 Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.
-Lemma persistently_sep `{BiPositive PROP} P Q :
-  bi_persistently (P ∗ Q) ⊣⊢ bi_persistently P ∗ bi_persistently Q.
+Lemma persistently_sep `{BiPositive PROP} P Q : <pers> (P ∗ Q) ⊣⊢ <pers> P ∗ <pers> Q.
 Proof.
   apply (anti_symm _); auto using persistently_sep_2.
   rewrite -persistently_affinely affinely_sep -and_sep_persistently. apply and_intro.
@@ -863,57 +842,51 @@ Proof.
   - by rewrite (affinely_elim_emp P) left_id affinely_elim.
 Qed.
 
-Lemma persistently_wand P Q :
-  bi_persistently (P -∗ Q) ⊢ bi_persistently P -∗ bi_persistently Q.
+Lemma persistently_wand P Q : <pers> (P -∗ Q) ⊢ <pers> P -∗ <pers> Q.
 Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
 
-Lemma persistently_entails_l P Q :
-  (P ⊢ bi_persistently Q) → P ⊢ bi_persistently Q ∗ P.
+Lemma persistently_entails_l P Q : (P ⊢ <pers> Q) → P ⊢ <pers> Q ∗ P.
 Proof. intros; rewrite -persistently_and_sep_l_1; auto. Qed.
-Lemma persistently_entails_r P Q :
-  (P ⊢ bi_persistently Q) → P ⊢ P ∗ bi_persistently Q.
+Lemma persistently_entails_r P Q : (P ⊢ <pers> Q) → P ⊢ P ∗ <pers> Q.
 Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed.
 
-Lemma persistently_impl_wand_2 P Q :
-  bi_persistently (P -∗ Q) ⊢ bi_persistently (P → Q).
+Lemma persistently_impl_wand_2 P Q : <pers> (P -∗ Q) ⊢ <pers> (P → Q).
 Proof.
   apply persistently_intro', impl_intro_r.
   rewrite -{2}(left_id emp%I _ P%I) persistently_and_sep_assoc.
   by rewrite (comm bi_and) persistently_and_emp_elim wand_elim_l.
 Qed.
 
-Lemma impl_wand_persistently_2 P Q : (bi_persistently P -∗ Q) ⊢ (bi_persistently P → Q).
+Lemma impl_wand_persistently_2 P Q : (<pers> P -∗ Q) ⊢ (<pers> P → Q).
 Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
 
 Section persistently_affinely_bi.
   Context `{BiAffine PROP}.
 
-  Lemma persistently_emp : bi_persistently emp ⊣⊢ emp.
+  Lemma persistently_emp : <pers> emp ⊣⊢ emp.
   Proof. by rewrite -!True_emp persistently_pure. Qed.
 
-  Lemma persistently_and_sep_l P Q :
-    bi_persistently P ∧ Q ⊣⊢ bi_persistently P ∗ Q.
+  Lemma persistently_and_sep_l P Q : <pers> P ∧ Q ⊣⊢ <pers> P ∗ Q.
   Proof.
     apply (anti_symm (⊢));
       eauto using persistently_and_sep_l_1, sep_and with typeclass_instances.
   Qed.
-  Lemma persistently_and_sep_r P Q : P ∧ bi_persistently Q ⊣⊢ P ∗ bi_persistently Q.
+  Lemma persistently_and_sep_r P Q : P ∧ <pers> Q ⊣⊢ P ∗ <pers> Q.
   Proof. by rewrite !(comm _ P) persistently_and_sep_l. Qed.
 
-  Lemma persistently_impl_wand P Q :
-    bi_persistently (P → Q) ⊣⊢ bi_persistently (P -∗ Q).
+  Lemma persistently_impl_wand P Q : <pers> (P → Q) ⊣⊢ <pers> (P -∗ Q).
   Proof.
     apply (anti_symm (⊢)); auto using persistently_impl_wand_2.
     apply persistently_intro', wand_intro_l.
     by rewrite -persistently_and_sep_r persistently_elim impl_elim_r.
   Qed.
 
-  Lemma impl_wand_persistently P Q : (bi_persistently P → Q) ⊣⊢ (bi_persistently P -∗ Q).
+  Lemma impl_wand_persistently P Q : (<pers> P → Q) ⊣⊢ (<pers> P -∗ Q).
   Proof.
     apply (anti_symm (⊢)). by rewrite -impl_wand_1. apply impl_wand_persistently_2.
   Qed.
 
-  Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ bi_persistently (P ∗ R → Q).
+  Lemma wand_alt P Q : (P -∗ Q) ⊣⊢ ∃ R, R ∗ <pers> (P ∗ R → Q).
   Proof.
     apply (anti_symm (⊢)).
     - rewrite -(right_id True%I bi_sep (P -∗ Q)%I) -(exist_intro (P -∗ Q)%I).
@@ -924,7 +897,7 @@ Section persistently_affinely_bi.
       rewrite assoc -persistently_and_sep_r.
       by rewrite persistently_elim impl_elim_r.
   Qed.
-  Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ bi_persistently (P ∧ R -∗ Q).
+  Lemma impl_alt P Q : (P → Q) ⊣⊢ ∃ R, R ∧ <pers> (P ∧ R -∗ Q).
   Proof.
     apply (anti_symm (⊢)).
     - rewrite -(right_id True%I bi_and (P → Q)%I) -(exist_intro (P → Q)%I).
@@ -961,16 +934,16 @@ Proof. by rewrite -affinely_sep -persistently_sep. Qed.
 Lemma affinely_persistently_idemp P : □ □ P ⊣⊢ □ P.
 Proof. by rewrite persistently_affinely persistently_idemp. Qed.
 
-Lemma persistently_and_affinely_sep_l P Q : bi_persistently P ∧ Q ⊣⊢ □ P ∗ Q.
+Lemma persistently_and_affinely_sep_l P Q : <pers> P ∧ Q ⊣⊢ □ P ∗ Q.
 Proof.
   apply (anti_symm _).
-  - by rewrite /bi_affinely -(comm bi_and (bi_persistently P))
+  - by rewrite /bi_affinely -(comm bi_and (<pers> P)%I)
       -persistently_and_sep_assoc left_id.
   - apply and_intro.
     + by rewrite affinely_elim persistently_absorbing.
     + by rewrite affinely_elim_emp left_id.
 Qed.
-Lemma persistently_and_affinely_sep_r P Q : P ∧ bi_persistently Q ⊣⊢ P ∗ □ Q.
+Lemma persistently_and_affinely_sep_r P Q : P ∧ <pers> Q ⊣⊢ P ∗ □ Q.
 Proof. by rewrite !(comm _ P) persistently_and_affinely_sep_l. Qed.
 Lemma and_sep_affinely_persistently P Q : □ P ∧ □ Q ⊣⊢ □ P ∗ □ Q.
 Proof.
@@ -982,7 +955,7 @@ Proof.
   by rewrite -persistently_and_affinely_sep_l affinely_and_r idemp.
 Qed.
 
-Lemma impl_wand_affinely_persistently P Q : (bi_persistently P → Q) ⊣⊢ (□ P -∗ Q).
+Lemma impl_wand_affinely_persistently P Q : (<pers> P → Q) ⊣⊢ (□ P -∗ Q).
 Proof.
   apply (anti_symm (⊢)).
   - apply wand_intro_l. by rewrite -persistently_and_affinely_sep_l impl_elim_r.
@@ -1000,40 +973,34 @@ Global Instance affinely_if_flip_mono' p :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_affinely_if PROP p).
 Proof. solve_proper. Qed.
 
-Lemma affinely_if_mono p P Q : (P ⊢ Q) → bi_affinely_if p P ⊢ bi_affinely_if p Q.
+Lemma affinely_if_mono p P Q : (P ⊢ Q) → <affine>?p P ⊢ <affine>?p Q.
 Proof. by intros ->. Qed.
-Lemma affinely_if_flag_mono (p q : bool) P :
-  (q → p) → bi_affinely_if p P ⊢ bi_affinely_if q P.
+Lemma affinely_if_flag_mono (p q : bool) P : (q → p) → <affine>?p P ⊢ <affine>?q P.
 Proof. destruct p, q; naive_solver auto using affinely_elim. Qed.
 
-Lemma affinely_if_elim p P : bi_affinely_if p P ⊢ P.
+Lemma affinely_if_elim p P : <affine>?p P ⊢ P.
 Proof. destruct p; simpl; auto using affinely_elim. Qed.
-Lemma affinely_affinely_if p P : bi_affinely P ⊢ bi_affinely_if p P.
+Lemma affinely_affinely_if p P : <affine> P ⊢ <affine>?p P.
 Proof. destruct p; simpl; auto using affinely_elim. Qed.
-Lemma affinely_if_intro' p P Q :
-  (bi_affinely_if p P ⊢ Q) → bi_affinely_if p P ⊢ bi_affinely_if p Q.
+Lemma affinely_if_intro' p P Q : (<affine>?p P ⊢ Q) → <affine>?p P ⊢ <affine>?p Q.
 Proof. destruct p; simpl; auto using affinely_intro'. Qed.
 
-Lemma affinely_if_emp p : bi_affinely_if p emp ⊣⊢ emp.
+Lemma affinely_if_emp p : <affine>?p emp ⊣⊢ emp.
 Proof. destruct p; simpl; auto using affinely_emp. Qed.
-Lemma affinely_if_and p P Q :
-  bi_affinely_if p (P ∧ Q) ⊣⊢ bi_affinely_if p P ∧ bi_affinely_if p Q.
+Lemma affinely_if_and p P Q : <affine>?p (P ∧ Q) ⊣⊢ <affine>?p P ∧ <affine>?p Q.
 Proof. destruct p; simpl; auto using affinely_and. Qed.
-Lemma affinely_if_or p P Q :
-  bi_affinely_if p (P ∨ Q) ⊣⊢ bi_affinely_if p P ∨ bi_affinely_if p Q.
+Lemma affinely_if_or p P Q : <affine>?p (P ∨ Q) ⊣⊢ <affine>?p P ∨ <affine>?p Q.
 Proof. destruct p; simpl; auto using affinely_or. Qed.
 Lemma affinely_if_exist {A} p (Ψ : A → PROP) :
-  bi_affinely_if p (∃ a, Ψ a) ⊣⊢ ∃ a, bi_affinely_if p (Ψ a).
+  <affine>?p (∃ a, Ψ a) ⊣⊢ ∃ a, <affine>?p (Ψ a).
 Proof. destruct p; simpl; auto using affinely_exist. Qed.
-Lemma affinely_if_sep_2 p P Q :
-  bi_affinely_if p P ∗ bi_affinely_if p Q ⊢ bi_affinely_if p (P ∗ Q).
+Lemma affinely_if_sep_2 p P Q : <affine>?p P ∗ <affine>?p Q ⊢ <affine>?p (P ∗ Q).
 Proof. destruct p; simpl; auto using affinely_sep_2. Qed.
 Lemma affinely_if_sep `{BiPositive PROP} p P Q :
-  bi_affinely_if p (P ∗ Q) ⊣⊢ bi_affinely_if p P ∗ bi_affinely_if p Q.
+  <affine>?p (P ∗ Q) ⊣⊢ <affine>?p P ∗ <affine>?p Q.
 Proof. destruct p; simpl; auto using affinely_sep. Qed.
 
-Lemma affinely_if_idemp p P :
-  bi_affinely_if p (bi_affinely_if p P) ⊣⊢ bi_affinely_if p P.
+Lemma affinely_if_idemp p P : <affine>?p <affine>?p P ⊣⊢ <affine>?p P.
 Proof. destruct p; simpl; auto using affinely_idemp. Qed.
 
 (* Conditional persistently *)
@@ -1049,30 +1016,25 @@ Global Instance persistently_if_flip_mono' p :
   Proper (flip (⊢) ==> flip (⊢)) (@bi_persistently_if PROP p).
 Proof. solve_proper. Qed.
 
-Lemma persistently_if_mono p P Q :
-  (P ⊢ Q) → bi_persistently_if p P ⊢ bi_persistently_if p Q.
+Lemma persistently_if_mono p P Q : (P ⊢ Q) → <pers>?p P ⊢ <pers>?p Q.
 Proof. by intros ->. Qed.
 
-Lemma persistently_if_pure p φ : bi_persistently_if p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Lemma persistently_if_pure p φ : <pers>?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
 Proof. destruct p; simpl; auto using persistently_pure. Qed.
-Lemma persistently_if_and p P Q :
-  bi_persistently_if p (P ∧ Q) ⊣⊢ bi_persistently_if p P ∧ bi_persistently_if p Q.
+Lemma persistently_if_and p P Q : <pers>?p (P ∧ Q) ⊣⊢ <pers>?p P ∧ <pers>?p Q.
 Proof. destruct p; simpl; auto using persistently_and. Qed.
-Lemma persistently_if_or p P Q :
-  bi_persistently_if p (P ∨ Q) ⊣⊢ bi_persistently_if p P ∨ bi_persistently_if p Q.
+Lemma persistently_if_or p P Q : <pers>?p (P ∨ Q) ⊣⊢ <pers>?p P ∨ <pers>?p Q.
 Proof. destruct p; simpl; auto using persistently_or. Qed.
 Lemma persistently_if_exist {A} p (Ψ : A → PROP) :
-  (bi_persistently_if p (∃ a, Ψ a)) ⊣⊢ ∃ a, bi_persistently_if p (Ψ a).
+  (<pers>?p (∃ a, Ψ a)) ⊣⊢ ∃ a, <pers>?p (Ψ a).
 Proof. destruct p; simpl; auto using persistently_exist. Qed.
-Lemma persistently_if_sep_2 p P Q :
-  bi_persistently_if p P ∗ bi_persistently_if p Q ⊢ bi_persistently_if p (P ∗ Q).
+Lemma persistently_if_sep_2 p P Q : <pers>?p P ∗ <pers>?p Q ⊢ <pers>?p (P ∗ Q).
 Proof. destruct p; simpl; auto using persistently_sep_2. Qed.
 Lemma persistently_if_sep `{BiPositive PROP} p P Q :
-  bi_persistently_if p (P ∗ Q) ⊣⊢ bi_persistently_if p P ∗ bi_persistently_if p Q.
+  <pers>?p (P ∗ Q) ⊣⊢ <pers>?p P ∗ <pers>?p Q.
 Proof. destruct p; simpl; auto using persistently_sep. Qed.
 
-Lemma persistently_if_idemp p P :
-  bi_persistently_if p (bi_persistently_if p P) ⊣⊢ bi_persistently_if p P.
+Lemma persistently_if_idemp p P : <pers>?p <pers>?p P ⊣⊢ <pers>?p P.
 Proof. destruct p; simpl; auto using persistently_idemp. Qed.
 
 (* Conditional affinely persistently *)
@@ -1111,31 +1073,28 @@ Proof. destruct p; simpl; auto using affinely_persistently_idemp. Qed.
 Global Instance Persistent_proper : Proper ((≡) ==> iff) (@Persistent PROP).
 Proof. solve_proper. Qed.
 
-Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ bi_persistently P.
+Lemma persistent_persistently_2 P `{!Persistent P} : P ⊢ <pers> P.
 Proof. done. Qed.
-Lemma persistent_persistently P `{!Persistent P, !Absorbing P} :
-  bi_persistently P ⊣⊢ P.
+Lemma persistent_persistently P `{!Persistent P, !Absorbing P} : <pers> P ⊣⊢ P.
 Proof.
   apply (anti_symm _); auto using persistent_persistently_2, persistently_elim.
 Qed.
 
-Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ bi_persistently Q.
+Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ <pers> Q.
 Proof. intros HP. by rewrite (persistent P) HP. Qed.
-Lemma persistent_and_affinely_sep_l_1 P Q `{!Persistent P} :
-  P ∧ Q ⊢ bi_affinely P ∗ Q.
+Lemma persistent_and_affinely_sep_l_1 P Q `{!Persistent P} : P ∧ Q ⊢ <affine> P ∗ Q.
 Proof.
   rewrite {1}(persistent_persistently_2 P) persistently_and_affinely_sep_l.
   by rewrite -affinely_idemp affinely_persistently_elim.
 Qed.
-Lemma persistent_and_affinely_sep_r_1 P Q `{!Persistent Q} :
-  P ∧ Q ⊢ P ∗ bi_affinely Q.
+Lemma persistent_and_affinely_sep_r_1 P Q `{!Persistent Q} : P ∧ Q ⊢ P ∗ <affine> Q.
 Proof. by rewrite !(comm _ P) persistent_and_affinely_sep_l_1. Qed.
 
 Lemma persistent_and_affinely_sep_l P Q `{!Persistent P, !Absorbing P} :
-  P ∧ Q ⊣⊢ bi_affinely P ∗ Q.
+  P ∧ Q ⊣⊢ <affine> P ∗ Q.
 Proof. by rewrite -(persistent_persistently P) persistently_and_affinely_sep_l. Qed.
 Lemma persistent_and_affinely_sep_r P Q `{!Persistent Q, !Absorbing Q} :
-  P ∧ Q ⊣⊢ P ∗ bi_affinely Q.
+  P ∧ Q ⊣⊢ P ∗ <affine> Q.
 Proof. by rewrite -(persistent_persistently Q) persistently_and_affinely_sep_r. Qed.
 
 Lemma persistent_and_sep_1 P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
@@ -1154,8 +1113,7 @@ Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 Lemma persistent_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
 Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 
-Lemma persistent_absorbingly_affinely P `{!Persistent P} :
-  P ⊢ bi_absorbingly (bi_affinely P).
+Lemma persistent_absorbingly_affinely P `{!Persistent P} : P ⊢ <absorb> <affine> P.
 Proof.
   by rewrite {1}(persistent_persistently_2 P) -persistently_affinely
              persistently_elim_absorbingly.
@@ -1201,7 +1159,7 @@ Proof. rewrite /Affine=> H. apply exist_elim=> a. by rewrite H. Qed.
 
 Global Instance sep_affine P Q : Affine P → Affine Q → Affine (P ∗ Q).
 Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed.
-Global Instance affinely_affine P : Affine (bi_affinely P).
+Global Instance affinely_affine P : Affine (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
 
 (* Absorbing instances *)
@@ -1240,12 +1198,12 @@ Global Instance wand_absorbing_r P Q : Absorbing Q → Absorbing (P -∗ Q).
 Proof. intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_intro. Qed.
 
 
-Global Instance absorbingly_absorbing P : Absorbing (bi_absorbingly P).
+Global Instance absorbingly_absorbing P : Absorbing (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
-Global Instance persistently_absorbing P : Absorbing (bi_persistently P).
+Global Instance persistently_absorbing P : Absorbing (<pers> P).
 Proof. by rewrite /Absorbing absorbingly_persistently. Qed.
 Global Instance persistently_if_absorbing P p :
-  Absorbing P → Absorbing (bi_persistently_if p P).
+  Absorbing P → Absorbing (<pers>?p P).
 Proof. intros; destruct p; simpl; apply _. Qed.
 
 (* Persistence instances *)
@@ -1276,11 +1234,11 @@ Global Instance sep_persistent P Q :
   Persistent P → Persistent Q → Persistent (P ∗ Q).
 Proof. intros. by rewrite /Persistent -persistently_sep_2 -!persistent. Qed.
 
-Global Instance persistently_persistent P : Persistent (bi_persistently P).
+Global Instance persistently_persistent P : Persistent (<pers> P).
 Proof. by rewrite /Persistent persistently_idemp. Qed.
-Global Instance affinely_persistent P : Persistent P → Persistent (bi_affinely P).
+Global Instance affinely_persistent P : Persistent P → Persistent (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
-Global Instance absorbingly_persistent P : Persistent P → Persistent (bi_absorbingly P).
+Global Instance absorbingly_persistent P : Persistent P → Persistent (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
@@ -1478,18 +1436,17 @@ Proof.
   intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
 Qed.
 
-Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : bi_absorbingly (x ≡ y) ⊣⊢ x ≡ y.
+Lemma absorbingly_internal_eq {A : ofeT} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
 Proof.
   apply (anti_symm _), absorbingly_intro.
   apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
   apply wand_intro_l, internal_eq_refl.
 Qed.
-Lemma persistently_internal_eq {A : ofeT} (a b : A) :
-  bi_persistently (a ≡ b) ⊣⊢ a ≡ b.
+Lemma persistently_internal_eq {A : ofeT} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
   apply (anti_symm (⊢)).
   { by rewrite persistently_elim_absorbingly absorbingly_internal_eq. }
-  apply (internal_eq_rewrite' a b (λ b, bi_persistently (a ≡ b))%I); auto.
+  apply (internal_eq_rewrite' a b (λ b, <pers> (a ≡ b))%I); auto.
   rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
 Qed.
 
@@ -1560,15 +1517,15 @@ Lemma later_wand P Q : ▷ (P -∗ Q) ⊢ ▷ P -∗ ▷ Q.
 Proof. apply wand_intro_l. by rewrite -later_sep wand_elim_r. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /bi_iff later_and !later_impl. Qed.
-Lemma later_persistently P : ▷ bi_persistently P ⊣⊢ bi_persistently (▷ P).
+Lemma later_persistently P : ▷ <pers> P ⊣⊢ <pers> ▷ P.
 Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
-Lemma later_affinely_2 P : bi_affinely (▷ P) ⊢ ▷ bi_affinely P.
+Lemma later_affinely_2 P : <affine> ▷ P ⊢ ▷ <affine> P.
 Proof. rewrite /bi_affinely later_and. auto using later_intro. Qed.
 Lemma later_affinely_persistently_2 P : □ ▷ P ⊢ ▷ □ P.
 Proof. by rewrite -later_persistently later_affinely_2. Qed.
 Lemma later_affinely_persistently_if_2 p P : □?p ▷ P ⊢ ▷ □?p P.
 Proof. destruct p; simpl; auto using later_affinely_persistently_2. Qed.
-Lemma later_absorbingly P : ▷ bi_absorbingly P ⊣⊢ bi_absorbingly (▷ P).
+Lemma later_absorbingly P : ▷ <absorb> P ⊣⊢ <absorb> ▷ P.
 Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
 
 Global Instance later_persistent P : Persistent P → Persistent (▷ P).
@@ -1627,15 +1584,15 @@ Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q.
 Proof. apply wand_intro_l. by rewrite -laterN_sep wand_elim_r. Qed.
 Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
 Proof. by rewrite /bi_iff laterN_and !laterN_impl. Qed.
-Lemma laterN_persistently n P : ▷^n bi_persistently P ⊣⊢ bi_persistently (▷^n P).
+Lemma laterN_persistently n P : ▷^n <pers> P ⊣⊢ <pers> ▷^n P.
 Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
-Lemma laterN_affinely_2 n P : bi_affinely (▷^n P) ⊢ ▷^n bi_affinely P.
+Lemma laterN_affinely_2 n P : <affine> ▷^n P ⊢ ▷^n <affine> P.
 Proof. rewrite /bi_affinely laterN_and. auto using laterN_intro. Qed.
 Lemma laterN_affinely_persistently_2 n P : □ ▷^n P ⊢ ▷^n □ P.
 Proof. by rewrite -laterN_persistently laterN_affinely_2. Qed.
 Lemma laterN_affinely_persistently_if_2 n p P : □?p ▷^n P ⊢ ▷^n □?p P.
 Proof. destruct p; simpl; auto using laterN_affinely_persistently_2. Qed.
-Lemma laterN_absorbingly n P : ▷^n (bi_absorbingly P) ⊣⊢ bi_absorbingly (▷^n P).
+Lemma laterN_absorbingly n P : ▷^n <absorb> P ⊣⊢ <absorb> ▷^n P.
 Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed.
 
 Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
@@ -1700,17 +1657,17 @@ Proof.
 Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /sbi_except_0 -later_or False_or. Qed.
-Lemma except_0_persistently P : ◇ bi_persistently P ⊣⊢ bi_persistently (◇ P).
+Lemma except_0_persistently P : ◇ <pers> P ⊣⊢ <pers> ◇ P.
 Proof.
   by rewrite /sbi_except_0 persistently_or -later_persistently persistently_pure.
 Qed.
-Lemma except_0_affinely_2 P : bi_affinely (◇ P) ⊢ ◇ bi_affinely P.
+Lemma except_0_affinely_2 P : <affine> ◇ P ⊢ ◇ <affine> P.
 Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed.
 Lemma except_0_affinely_persistently_2 P : □ ◇ P ⊢ ◇ □ P.
 Proof. by rewrite -except_0_persistently except_0_affinely_2. Qed.
 Lemma except_0_affinely_persistently_if_2 p P : □?p ◇ P ⊢ ◇ □?p P.
 Proof. destruct p; simpl; auto using except_0_affinely_persistently_2. Qed.
-Lemma except_0_absorbingly P : ◇ (bi_absorbingly P) ⊣⊢ bi_absorbingly (◇ P).
+Lemma except_0_absorbingly P : ◇ <absorb> P ⊣⊢ <absorb> ◇ P.
 Proof. by rewrite /bi_absorbingly except_0_sep except_0_True. Qed.
 
 Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
@@ -1718,8 +1675,7 @@ Proof. by rewrite {1}(except_0_intro P) except_0_sep. Qed.
 Lemma except_0_frame_r P Q : ◇ P ∗ Q ⊢ ◇ (P ∗ Q).
 Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
 
-Lemma later_affinely_1 `{!Timeless (emp%I : PROP)} P :
-  ▷ bi_affinely P ⊢ ◇ bi_affinely (▷ P).
+Lemma later_affinely_1 `{!Timeless (emp%I : PROP)} P : ▷ <affine> P ⊢ ◇ <affine> ▷ P.
 Proof.
   rewrite /bi_affinely later_and (timeless emp%I) except_0_and.
   by apply and_mono, except_0_intro.
@@ -1781,16 +1737,16 @@ Proof.
   - rewrite /sbi_except_0; auto.
   - apply exist_elim=> x. rewrite -(exist_intro x); auto.
 Qed.
-Global Instance persistently_timeless P : Timeless P → Timeless (bi_persistently P).
+Global Instance persistently_timeless P : Timeless P → Timeless (<pers> P).
 Proof.
   intros. rewrite /Timeless /sbi_except_0 later_persistently_1.
   by rewrite (timeless P) /sbi_except_0 persistently_or {1}persistently_elim.
 Qed.
 
 Global Instance affinely_timeless P :
-  Timeless (emp%I : PROP) → Timeless P → Timeless (bi_affinely P).
+  Timeless (emp%I : PROP) → Timeless P → Timeless (<affine> P).
 Proof. rewrite /bi_affinely; apply _. Qed.
-Global Instance absorbingly_timeless P : Timeless P → Timeless (bi_absorbingly P).
+Global Instance absorbingly_timeless P : Timeless P → Timeless (<absorb> P).
 Proof. rewrite /bi_absorbingly; apply _. Qed.
 
 Global Instance eq_timeless {A : ofeT} (a b : A) :
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 01b0c0175655a414e26e1110f872a5cb79e085f8..247c09ff72a2835a92f66d365fc70eb3b326ee8b 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -22,7 +22,7 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
   bi_embed_mixin_exist_1 A (Φ : A → PROP1) : ⎡∃ x, Φ x⎤ ⊢ ∃ x, ⎡Φ x⎤;
   bi_embed_mixin_sep P Q : ⎡P ∗ Q⎤ ⊣⊢ ⎡P⎤ ∗ ⎡Q⎤;
   bi_embed_mixin_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤;
-  bi_embed_mixin_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤
+  bi_embed_mixin_persistently P : ⎡<pers> P⎤ ⊣⊢ <pers> ⎡P⎤
 }.
 
 Class BiEmbed (PROP1 PROP2 : bi) := {
@@ -79,7 +79,7 @@ Section embed_laws.
   Proof. eapply bi_embed_mixin_sep, bi_embed_mixin. Qed.
   Lemma embed_wand_2 P Q : (⎡P⎤ -∗ ⎡Q⎤) ⊢ ⎡P -∗ Q⎤.
   Proof. eapply bi_embed_mixin_wand_2, bi_embed_mixin. Qed.
-  Lemma embed_persistently P : ⎡bi_persistently P⎤ ⊣⊢ bi_persistently ⎡P⎤.
+  Lemma embed_persistently P : ⎡<pers> P⎤ ⊣⊢ <pers> ⎡P⎤.
   Proof. eapply bi_embed_mixin_persistently, bi_embed_mixin. Qed.
 End embed_laws.
 
@@ -141,14 +141,13 @@ Section embed.
   Proof. by rewrite embed_and !embed_impl. Qed.
   Lemma embed_wand_iff P Q : ⎡P ∗-∗ Q⎤ ⊣⊢ (⎡P⎤ ∗-∗ ⎡Q⎤).
   Proof. by rewrite embed_and !embed_wand. Qed.
-  Lemma embed_affinely P : ⎡bi_affinely P⎤ ⊣⊢ bi_affinely ⎡P⎤.
+  Lemma embed_affinely P : ⎡<affine> P⎤ ⊣⊢ <affine> ⎡P⎤.
   Proof. by rewrite embed_and embed_emp. Qed.
-  Lemma embed_absorbingly P : ⎡bi_absorbingly P⎤ ⊣⊢ bi_absorbingly ⎡P⎤.
+  Lemma embed_absorbingly P : ⎡<absorb> P⎤ ⊣⊢ <absorb> ⎡P⎤.
   Proof. by rewrite embed_sep embed_pure. Qed.
-  Lemma embed_persistently_if P b :
-    ⎡bi_persistently_if b P⎤ ⊣⊢ bi_persistently_if b ⎡P⎤.
+  Lemma embed_persistently_if P b : ⎡<pers>?b P⎤ ⊣⊢ <pers>?b ⎡P⎤.
   Proof. destruct b; simpl; auto using embed_persistently. Qed.
-  Lemma embed_affinely_if P b : ⎡bi_affinely_if b P⎤ ⊣⊢ bi_affinely_if b ⎡P⎤.
+  Lemma embed_affinely_if P b : ⎡<affine>?b P⎤ ⊣⊢ <affine>?b ⎡P⎤.
   Proof. destruct b; simpl; auto using embed_affinely. Qed.
   Lemma embed_hforall {As} (Φ : himpl As PROP1):
     ⎡bi_hforall Φ⎤ ⊣⊢ bi_hforall (hcompose embed Φ).
@@ -233,6 +232,6 @@ End sbi_embed.
 
 (* Not defined using an ordinary [Instance] because the default
 [class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
-search for the other premises fail. See the proof of [monPred_absolutely_plain]
+search for the other premises fail. See the proof of [monPred_objectively_plain]
 for an example where it would fail with a regular [Instance].*)
 Hint Extern 4 (Plain ⎡_⎤) => eapply @embed_plain : typeclass_instances.
diff --git a/theories/bi/fixpoint.v b/theories/bi/fixpoint.v
index ec42bf3236b8562b57d72048d93e014d5d763917..43f506b7b1ea615ffe26900b9942fe116df8b9b9 100644
--- a/theories/bi/fixpoint.v
+++ b/theories/bi/fixpoint.v
@@ -6,7 +6,7 @@ Import bi.
 (** Least and greatest fixpoint of a monotone function, defined entirely inside
     the logic.  *)
 Class BiMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := {
-  bi_mono_pred Φ Ψ : ((bi_persistently (∀ x, Φ x -∗ Ψ x)) → ∀ x, F Φ x -∗ F Ψ x)%I;
+  bi_mono_pred Φ Ψ : (<pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I;
   bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
 }.
 Arguments bi_mono_pred {_ _ _ _} _ _.
@@ -14,11 +14,11 @@ Local Existing Instance bi_mono_pred_ne.
 
 Definition bi_least_fixpoint {PROP : bi} {A : ofeT}
     (F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
-  (∀ Φ : A -n> PROP, bi_persistently (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
+  (∀ Φ : A -n> PROP, <pers> (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
 
 Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
     (F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
-  (∃ Φ : A -n> PROP, bi_persistently (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
+  (∃ Φ : A -n> PROP, <pers> (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
 
 Section least.
   Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 5fd4fa0e9276b76487da0cfcda71b188aac3e68b..955c22d4282e86dd1bec9931124f74fcc713792f 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -6,6 +6,7 @@ Reserved Notation "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
 Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "'<pers>' P" (at level 20, right associativity).
 Reserved Notation "â–· P" (at level 20, right associativity).
 
 Section bi_mixin.
@@ -38,6 +39,7 @@ Section bi_mixin.
     (bi_exist _ (λ x, .. (bi_exist _ (λ y, P)) ..)).
   Local Infix "∗" := bi_sep.
   Local Infix "-∗" := bi_wand.
+  Local Notation "'<pers>' P" := (bi_persistently P).
   Local Notation "x ≡ y" := (sbi_internal_eq _ x y).
   Local Notation "â–· P" := (sbi_later P).
 
@@ -102,27 +104,23 @@ Section bi_mixin.
 
     (* Persistently *)
     (* In the ordered RA model: Holds without further assumptions. *)
-    bi_mixin_persistently_mono P Q :
-      (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q;
+    bi_mixin_persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q;
     (* In the ordered RA model: `core` is idempotent *)
-    bi_mixin_persistently_idemp_2 P :
-      bi_persistently P ⊢ bi_persistently (bi_persistently P);
+    bi_mixin_persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P;
 
     (* In the ordered RA model: `ε ≼ core x` *)
-    bi_mixin_persistently_emp_intro P : P ⊢ bi_persistently emp;
+    bi_mixin_persistently_emp_intro P : P ⊢ <pers> emp;
 
     bi_mixin_persistently_forall_2 {A} (Ψ : A → PROP) :
-      (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a);
+      (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a);
     bi_mixin_persistently_exist_1 {A} (Ψ : A → PROP) :
-      bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a);
+      <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a);
 
     (* In the ordered RA model: [core x ≼ core (x ⋅ y)].
        Note that this implies that the core is monotone. *)
-    bi_mixin_persistently_absorbing P Q :
-      bi_persistently P ∗ Q ⊢ bi_persistently P;
+    bi_mixin_persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P;
     (* In the ordered RA model: [x â‹… core x = core x]. *)
-    bi_mixin_persistently_and_sep_elim P Q :
-      bi_persistently P ∧ Q ⊢ P ∗ Q;
+    bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
   }.
 
   Record SbiMixin := {
@@ -149,10 +147,8 @@ Section bi_mixin.
       (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a);
     sbi_mixin_later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
     sbi_mixin_later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q);
-    sbi_mixin_later_persistently_1 P :
-      ▷ bi_persistently P ⊢ bi_persistently (▷ P);
-    sbi_mixin_later_persistently_2 P :
-      bi_persistently (▷ P) ⊢ ▷ bi_persistently P;
+    sbi_mixin_later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P;
+    sbi_mixin_later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P;
 
     sbi_mixin_later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P);
   }.
@@ -292,6 +288,7 @@ Notation "∀ x .. y , P" :=
   (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.
 Notation "∃ x .. y , P" :=
   (bi_exist (λ x, .. (bi_exist (λ y, P)) ..)%I) : bi_scope.
+Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
 
 Infix "≡" := sbi_internal_eq : bi_scope.
 Notation "â–· P" := (sbi_later P) : bi_scope.
@@ -391,25 +388,24 @@ Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
 Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
 
 (* Persistently *)
-Lemma persistently_mono P Q : (P ⊢ Q) → bi_persistently P ⊢ bi_persistently Q.
+Lemma persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q.
 Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
-Lemma persistently_idemp_2 P :
-  bi_persistently P ⊢ bi_persistently (bi_persistently P).
+Lemma persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P.
 Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
 
-Lemma persistently_emp_intro P : P ⊢ bi_persistently emp.
+Lemma persistently_emp_intro P : P ⊢ <pers> emp.
 Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
 
 Lemma persistently_forall_2 {A} (Ψ : A → PROP) :
-  (∀ a, bi_persistently (Ψ a)) ⊢ bi_persistently (∀ a, Ψ a).
+  (∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a).
 Proof. eapply bi_mixin_persistently_forall_2, bi_bi_mixin. Qed.
 Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
-  bi_persistently (∃ a, Ψ a) ⊢ ∃ a, bi_persistently (Ψ a).
+  <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a).
 Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
 
-Lemma persistently_absorbing P Q : bi_persistently P ∗ Q ⊢ bi_persistently P.
+Lemma persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P.
 Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
-Lemma persistently_and_sep_elim P Q : bi_persistently P ∧ Q ⊢ P ∗ Q.
+Lemma persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q.
 Proof. eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_mixin. Qed.
 End bi_laws.
 
@@ -459,9 +455,9 @@ Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
 Proof. eapply sbi_mixin_later_sep_1, sbi_sbi_mixin. Qed.
 Lemma later_sep_2 P Q : ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q).
 Proof. eapply sbi_mixin_later_sep_2, sbi_sbi_mixin. Qed.
-Lemma later_persistently_1 P : ▷ bi_persistently P ⊢ bi_persistently (▷ P).
+Lemma later_persistently_1 P : ▷ <pers> P ⊢ <pers> ▷ P.
 Proof. eapply (sbi_mixin_later_persistently_1 bi_entails), sbi_sbi_mixin. Qed.
-Lemma later_persistently_2 P : bi_persistently (▷ P) ⊢ ▷ bi_persistently P.
+Lemma later_persistently_2 P : <pers> ▷ P ⊢ ▷ <pers> P.
 Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
 
 Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 0085af57a38f031b65e9ffe7d64ba2dac1ca814d..11b0f5f999e144f9ab6ed45a50921242b1043af0 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -140,15 +140,15 @@ Definition monPred_pure_aux : seal (@monPred_pure_def). by eexists. Qed.
 Definition monPred_pure := unseal monPred_pure_aux.
 Definition monPred_pure_eq : @monPred_pure = _ := seal_eq _.
 
-Definition monPred_absolutely_def P : monPred := MonPred (λ _, ∀ i, P i)%I _.
-Definition monPred_absolutely_aux : seal (@monPred_absolutely_def). by eexists. Qed.
-Definition monPred_absolutely := unseal monPred_absolutely_aux.
-Definition monPred_absolutely_eq : @monPred_absolutely = _ := seal_eq _.
+Definition monPred_objectively_def P : monPred := MonPred (λ _, ∀ i, P i)%I _.
+Definition monPred_objectively_aux : seal (@monPred_objectively_def). by eexists. Qed.
+Definition monPred_objectively := unseal monPred_objectively_aux.
+Definition monPred_objectively_eq : @monPred_objectively = _ := seal_eq _.
 
-Definition monPred_relatively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _.
-Definition monPred_relatively_aux : seal (@monPred_relatively_def). by eexists. Qed.
-Definition monPred_relatively := unseal monPred_relatively_aux.
-Definition monPred_relatively_eq : @monPred_relatively = _ := seal_eq _.
+Definition monPred_subjectively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _.
+Definition monPred_subjectively_aux : seal (@monPred_subjectively_def). by eexists. Qed.
+Definition monPred_subjectively := unseal monPred_subjectively_aux.
+Definition monPred_subjectively_eq : @monPred_subjectively = _ := seal_eq _.
 
 Program Definition monPred_and_def P Q : monPred :=
   MonPred (λ i, P i ∧ Q i)%I _.
@@ -198,7 +198,7 @@ Definition monPred_wand := unseal monPred_wand_aux.
 Definition monPred_wand_eq : @monPred_wand = _ := seal_eq _.
 
 Program Definition monPred_persistently_def P : monPred :=
-  MonPred (λ i, bi_persistently (P i)) _.
+  MonPred (λ i, <pers> (P i))%I _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_persistently_aux : seal (@monPred_persistently_def). by eexists. Qed.
 Definition monPred_persistently := unseal monPred_persistently_aux.
@@ -222,10 +222,10 @@ Definition monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux.
 Definition monPred_bupd_eq `{BUpd PROP} : @bupd _ monPred_bupd = _ := seal_eq _.
 End Bi.
 
-Arguments monPred_absolutely {_ _} _%I.
-Arguments monPred_relatively {_ _} _%I.
-Notation "'∀ᵢ' P" := (monPred_absolutely P) (at level 20, right associativity) : bi_scope.
-Notation "'∃ᵢ' P" := (monPred_relatively P) (at level 20, right associativity) : bi_scope.
+Arguments monPred_objectively {_ _} _%I.
+Arguments monPred_subjectively {_ _} _%I.
+Notation "'<obj>' P" := (monPred_objectively P) (at level 20, right associativity) : bi_scope.
+Notation "'<subj>' P" := (monPred_subjectively P) (at level 20, right associativity) : bi_scope.
 
 Section Sbi.
 Context {I : biIndex} {PROP : sbi}.
@@ -267,7 +267,7 @@ Definition unseal_eqs :=
    @monPred_sep_eq, @monPred_wand_eq,
    @monPred_persistently_eq, @monPred_later_eq, @monPred_internal_eq_eq, @monPred_in_eq,
    @monPred_embed_eq, @monPred_emp_eq, @monPred_pure_eq, @monPred_plainly_eq,
-   @monPred_absolutely_eq, @monPred_relatively_eq, @monPred_bupd_eq, @monPred_fupd_eq).
+   @monPred_objectively_eq, @monPred_subjectively_eq, @monPred_bupd_eq, @monPred_fupd_eq).
 Ltac unseal :=
   unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
          monPred_upclosed, bi_and, bi_or,
@@ -419,12 +419,12 @@ Proof.
 Qed.
 End canonical_sbi.
 
-Class Absolute {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
-  absolute_at i j : P i -∗ P j.
-Arguments Absolute {_ _} _%I.
-Arguments absolute_at {_ _} _%I {_}.
-Hint Mode Absolute + + ! : typeclass_instances.
-Instance: Params (@Absolute) 2.
+Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
+  objective_at i j : P i -∗ P j.
+Arguments Objective {_ _} _%I.
+Arguments objective_at {_ _} _%I {_}.
+Hint Mode Objective + + ! : typeclass_instances.
+Instance: Params (@Objective) 2.
 
 (** Primitive facts that cannot be deduced from the BI structure. *)
 
@@ -491,48 +491,48 @@ Lemma monPred_emp_unfold : emp%I = ⎡emp : PROP⎤%I.
 Proof. by unseal. Qed.
 Lemma monPred_pure_unfold : bi_pure = λ φ, ⎡ ⌜ φ ⌝ : PROP⎤%I.
 Proof. by unseal. Qed.
-Lemma monPred_absolutely_unfold : monPred_absolutely = λ P, ⎡∀ i, P i⎤%I.
+Lemma monPred_objectively_unfold : monPred_objectively = λ P, ⎡∀ i, P i⎤%I.
 Proof. by unseal. Qed.
-Lemma monPred_relatively_unfold : monPred_relatively = λ P, ⎡∃ i, P i⎤%I.
+Lemma monPred_subjectively_unfold : monPred_subjectively = λ P, ⎡∃ i, P i⎤%I.
 Proof. by unseal. Qed.
 
-Global Instance monPred_absolutely_ne : NonExpansive (@monPred_absolutely I PROP).
-Proof. rewrite monPred_absolutely_unfold. solve_proper. Qed.
-Global Instance monPred_absolutely_proper : Proper ((≡) ==> (≡)) (@monPred_absolutely I PROP).
+Global Instance monPred_objectively_ne : NonExpansive (@monPred_objectively I PROP).
+Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
+Global Instance monPred_objectively_proper : Proper ((≡) ==> (≡)) (@monPred_objectively I PROP).
 Proof. apply (ne_proper _). Qed.
-Lemma monPred_absolutely_mono P Q : (P ⊢ Q) → (∀ᵢ P ⊢ ∀ᵢ Q).
-Proof. rewrite monPred_absolutely_unfold. solve_proper. Qed.
-Global Instance monPred_absolutely_mono' : Proper ((⊢) ==> (⊢)) (@monPred_absolutely I PROP).
-Proof. intros ???. by apply monPred_absolutely_mono. Qed.
-Global Instance monPred_absolutely_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@monPred_absolutely I PROP).
-Proof. intros ???. by apply monPred_absolutely_mono. Qed.
-
-Global Instance monPred_absolutely_persistent P : Persistent P → Persistent (∀ᵢ P).
-Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
-Global Instance monPred_absolutely_absorbing P : Absorbing P → Absorbing (∀ᵢ P).
-Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
-Global Instance monPred_absolutely_affine P : Affine P → Affine (∀ᵢ P).
-Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
-
-Global Instance monPred_relatively_ne : NonExpansive (@monPred_relatively I PROP).
-Proof. rewrite monPred_relatively_unfold. solve_proper. Qed.
-Global Instance monPred_relatively_proper : Proper ((≡) ==> (≡)) (@monPred_relatively I PROP).
+Lemma monPred_objectively_mono P Q : (P ⊢ Q) → (<obj> P ⊢ <obj> Q).
+Proof. rewrite monPred_objectively_unfold. solve_proper. Qed.
+Global Instance monPred_objectively_mono' : Proper ((⊢) ==> (⊢)) (@monPred_objectively I PROP).
+Proof. intros ???. by apply monPred_objectively_mono. Qed.
+Global Instance monPred_objectively_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@monPred_objectively I PROP).
+Proof. intros ???. by apply monPred_objectively_mono. Qed.
+
+Global Instance monPred_objectively_persistent P : Persistent P → Persistent (<obj> P).
+Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+Global Instance monPred_objectively_absorbing P : Absorbing P → Absorbing (<obj> P).
+Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+Global Instance monPred_objectively_affine P : Affine P → Affine (<obj> P).
+Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+
+Global Instance monPred_subjectively_ne : NonExpansive (@monPred_subjectively I PROP).
+Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
+Global Instance monPred_subjectively_proper : Proper ((≡) ==> (≡)) (@monPred_subjectively I PROP).
 Proof. apply (ne_proper _). Qed.
-Lemma monPred_relatively_mono P Q : (P ⊢ Q) → (∃ᵢ P ⊢ ∃ᵢ Q).
-Proof. rewrite monPred_relatively_unfold. solve_proper. Qed.
-Global Instance monPred_relatively_mono' : Proper ((⊢) ==> (⊢)) (@monPred_relatively I PROP).
-Proof. intros ???. by apply monPred_relatively_mono. Qed.
-Global Instance monPred_relatively_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@monPred_relatively I PROP).
-Proof. intros ???. by apply monPred_relatively_mono. Qed.
-
-Global Instance monPred_relatively_persistent P : Persistent P → Persistent (∃ᵢ P).
-Proof. rewrite monPred_relatively_unfold. apply _. Qed.
-Global Instance monPred_relatively_absorbing P : Absorbing P → Absorbing (∃ᵢ P).
-Proof. rewrite monPred_relatively_unfold. apply _. Qed.
-Global Instance monPred_relatively_affine P : Affine P → Affine (∃ᵢ P).
-Proof. rewrite monPred_relatively_unfold. apply _. Qed.
+Lemma monPred_subjectively_mono P Q : (P ⊢ Q) → <subj> P ⊢ <subj> Q.
+Proof. rewrite monPred_subjectively_unfold. solve_proper. Qed.
+Global Instance monPred_subjectively_mono' : Proper ((⊢) ==> (⊢)) (@monPred_subjectively I PROP).
+Proof. intros ???. by apply monPred_subjectively_mono. Qed.
+Global Instance monPred_subjectively_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@monPred_subjectively I PROP).
+Proof. intros ???. by apply monPred_subjectively_mono. Qed.
+
+Global Instance monPred_subjectively_persistent P : Persistent P → Persistent (<subj> P).
+Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
+Global Instance monPred_subjectively_absorbing P : Absorbing P → Absorbing (<subj> P).
+Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
+Global Instance monPred_subjectively_affine P : Affine P → Affine (<subj> P).
+Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
 
 (** monPred_at unfolding laws *)
 Lemma monPred_at_embed i (P : PROP) : monPred_at ⎡P⎤ i ⊣⊢ P.
@@ -555,23 +555,21 @@ Lemma monPred_at_sep i P Q : (P ∗ Q) i ⊣⊢ P i ∗ Q i.
 Proof. by unseal. Qed.
 Lemma monPred_at_wand i P Q : (P -∗ Q) i ⊣⊢ ∀ j, ⌜i ⊑ j⌝ → P j -∗ Q j.
 Proof. by unseal. Qed.
-Lemma monPred_at_persistently i P : bi_persistently P i ⊣⊢ bi_persistently (P i).
+Lemma monPred_at_persistently i P : (<pers> P) i ⊣⊢ <pers> (P i).
 Proof. by unseal. Qed.
 Lemma monPred_at_in i j : monPred_at (monPred_in j) i ⊣⊢ ⌜j ⊑ i⌝.
 Proof. by unseal. Qed.
-Lemma monPred_at_absolutely i P : (∀ᵢ P) i ⊣⊢ ∀ j, P j.
+Lemma monPred_at_objectively i P : (<obj> P) i ⊣⊢ ∀ j, P j.
 Proof. by unseal. Qed.
-Lemma monPred_at_relatively i P : (∃ᵢ P) i ⊣⊢ ∃ j, P j.
+Lemma monPred_at_subjectively i P : (<subj> P) i ⊣⊢ ∃ j, P j.
 Proof. by unseal. Qed.
-Lemma monPred_at_persistently_if i p P :
-  bi_persistently_if p P i ⊣⊢ bi_persistently_if p (P i).
+Lemma monPred_at_persistently_if i p P : (<pers>?p P) i ⊣⊢ <pers>?p (P i).
 Proof. destruct p=>//=. apply monPred_at_persistently. Qed.
-Lemma monPred_at_affinely i P : bi_affinely P i ⊣⊢ bi_affinely (P i).
+Lemma monPred_at_affinely i P : (<affine> P) i ⊣⊢ <affine> (P i).
 Proof. by rewrite /bi_affinely monPred_at_and monPred_at_emp. Qed.
-Lemma monPred_at_affinely_if i p P :
-  bi_affinely_if p P i ⊣⊢ bi_affinely_if p (P i).
+Lemma monPred_at_affinely_if i p P : (<affine>?p P) i ⊣⊢ <affine>?p (P i).
 Proof. destruct p=>//=. apply monPred_at_affinely. Qed.
-Lemma monPred_at_absorbingly i P : bi_absorbingly P i ⊣⊢ bi_absorbingly (P i).
+Lemma monPred_at_absorbingly i P : (<absorb> P) i ⊣⊢ <absorb> (P i).
 Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
 
 Lemma monPred_wand_force i P Q : (P -∗ Q) i -∗ (P i -∗ Q i).
@@ -579,141 +577,137 @@ Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed
 Lemma monPred_impl_force i P Q : (P → Q) i -∗ (P i → Q i).
 Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
 
-(* Laws for monPred_absolutely and of Absolute. *)
-Lemma monPred_absolutely_elim P : ∀ᵢ P ⊢ P.
-Proof. rewrite monPred_absolutely_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
-Lemma monPred_absolutely_idemp P : ∀ᵢ (∀ᵢ P) ⊣⊢ ∀ᵢ P.
+(* Laws for monPred_objectively and of Objective. *)
+Lemma monPred_objectively_elim P : <obj> P ⊢ P.
+Proof. rewrite monPred_objectively_unfold. unseal. split=>?. apply bi.forall_elim. Qed.
+Lemma monPred_objectively_idemp P : <obj> <obj> P ⊣⊢ <obj> P.
 Proof.
-  apply bi.equiv_spec; split; [by apply monPred_absolutely_elim|].
+  apply bi.equiv_spec; split; [by apply monPred_objectively_elim|].
   unseal. split=>i /=. by apply bi.forall_intro=>_.
 Qed.
 
-Lemma monPred_absolutely_forall {A} (Φ : A → monPred) : ∀ᵢ (∀ x, Φ x) ⊣⊢ ∀ x, ∀ᵢ (Φ x).
+Lemma monPred_objectively_forall {A} (Φ : A → monPred) : <obj> (∀ x, Φ x) ⊣⊢ ∀ x, <obj> (Φ x).
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=;
     do 2 apply bi.forall_intro=>?; by do 2 rewrite bi.forall_elim.
 Qed.
-Lemma monPred_absolutely_and P Q : ∀ᵢ (P ∧ Q) ⊣⊢ ∀ᵢ P ∧ ∀ᵢ Q.
+Lemma monPred_objectively_and P Q : <obj> (P ∧ Q) ⊣⊢ <obj> P ∧ <obj> Q.
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=.
   - apply bi.and_intro; do 2 f_equiv. apply bi.and_elim_l. apply bi.and_elim_r.
   - apply bi.forall_intro=>?. by rewrite !bi.forall_elim.
 Qed.
-Lemma monPred_absolutely_exist {A} (Φ : A → monPred) :
-  (∃ x, ∀ᵢ (Φ x)) ⊢ ∀ᵢ (∃ x, (Φ x)).
+Lemma monPred_objectively_exist {A} (Φ : A → monPred) :
+  (∃ x, <obj> (Φ x)) ⊢ <obj> (∃ x, (Φ x)).
 Proof. apply bi.exist_elim=>?. f_equiv. apply bi.exist_intro. Qed.
-Lemma monPred_absolutely_or P Q : (∀ᵢ P) ∨ (∀ᵢ Q) ⊢ ∀ᵢ (P ∨ Q).
+Lemma monPred_objectively_or P Q : <obj> P ∨ <obj> Q ⊢ <obj> (P ∨ Q).
 Proof. apply bi.or_elim; f_equiv. apply bi.or_intro_l. apply bi.or_intro_r. Qed.
 
-Lemma monPred_absolutely_sep_2 P Q : ∀ᵢ P ∗ ∀ᵢ Q ⊢ ∀ᵢ (P ∗ Q).
+Lemma monPred_objectively_sep_2 P Q : <obj> P ∗ <obj> Q ⊢ <obj> (P ∗ Q).
 Proof. unseal. split=>i /=. apply bi.forall_intro=>?. by rewrite !bi.forall_elim. Qed.
-Lemma monPred_absolutely_sep `{BiIndexBottom bot} P Q : ∀ᵢ (P ∗ Q) ⊣⊢ ∀ᵢ P ∗ ∀ᵢ Q.
+Lemma monPred_objectively_sep `{BiIndexBottom bot} P Q : <obj> (P ∗ Q) ⊣⊢ <obj> P ∗ <obj> Q.
 Proof.
-  apply bi.equiv_spec, conj, monPred_absolutely_sep_2. unseal. split=>i /=.
+  apply bi.equiv_spec, conj, monPred_objectively_sep_2. unseal. split=>i /=.
   rewrite (bi.forall_elim bot). by f_equiv; apply bi.forall_intro=>j; f_equiv.
 Qed.
-Lemma monPred_absolutely_embed (P : PROP) : ∀ᵢ ⎡P⎤ ⊣⊢ ⎡P⎤.
+Lemma monPred_objectively_embed (P : PROP) : <obj> ⎡P⎤ ⊣⊢ ⎡P⎤.
 Proof.
   apply bi.equiv_spec; split; unseal; split=>i /=.
   by rewrite (bi.forall_elim inhabitant). by apply bi.forall_intro.
 Qed.
-Lemma monPred_absolutely_emp : ∀ᵢ (emp : monPred) ⊣⊢ emp.
-Proof. rewrite monPred_emp_unfold. apply monPred_absolutely_embed. Qed.
-Lemma monPred_absolutely_pure φ : ∀ᵢ (⌜ φ ⌝ : monPred) ⊣⊢ ⌜ φ ⌝.
-Proof. rewrite monPred_pure_unfold. apply monPred_absolutely_embed. Qed.
+Lemma monPred_objectively_emp : <obj> (emp : monPred) ⊣⊢ emp.
+Proof. rewrite monPred_emp_unfold. apply monPred_objectively_embed. Qed.
+Lemma monPred_objectively_pure φ : <obj> (⌜ φ ⌝ : monPred) ⊣⊢ ⌜ φ ⌝.
+Proof. rewrite monPred_pure_unfold. apply monPred_objectively_embed. Qed.
 
-Lemma monPred_relatively_intro P : P ⊢ ∃ᵢ P.
+Lemma monPred_subjectively_intro P : P ⊢ <subj> P.
 Proof. unseal. split=>?. apply bi.exist_intro. Qed.
 
-Lemma monPred_relatively_forall {A} (Φ : A → monPred) :
-  (∃ᵢ (∀ x, Φ x)) ⊢ ∀ x, ∃ᵢ (Φ x).
+Lemma monPred_subjectively_forall {A} (Φ : A → monPred) :
+  (<subj> (∀ x, Φ x)) ⊢ ∀ x, <subj> (Φ x).
 Proof. apply bi.forall_intro=>?. f_equiv. apply bi.forall_elim. Qed.
-Lemma monPred_relatively_and P Q : ∃ᵢ (P ∧ Q) ⊢ (∃ᵢ P) ∧ (∃ᵢ Q).
+Lemma monPred_subjectively_and P Q : <subj> (P ∧ Q) ⊢ <subj> P ∧ <subj> Q.
 Proof. apply bi.and_intro; f_equiv. apply bi.and_elim_l. apply bi.and_elim_r. Qed.
-Lemma monPred_relatively_exist {A} (Φ : A → monPred) : ∃ᵢ (∃ x, Φ x) ⊣⊢ ∃ x, ∃ᵢ (Φ x).
+Lemma monPred_subjectively_exist {A} (Φ : A → monPred) : <subj> (∃ x, Φ x) ⊣⊢ ∃ x, <subj> (Φ x).
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=;
     do 2 apply bi.exist_elim=>?; by do 2 rewrite -bi.exist_intro.
 Qed.
-Lemma monPred_relatively_or P Q : ∃ᵢ (P ∨ Q) ⊣⊢ ∃ᵢ P ∨ ∃ᵢ Q.
+Lemma monPred_subjectively_or P Q : <subj> (P ∨ Q) ⊣⊢ <subj> P ∨ <subj> Q.
 Proof.
   unseal. split=>i. apply bi.equiv_spec; split=>/=.
   - apply bi.exist_elim=>?. by rewrite -!bi.exist_intro.
   - apply bi.or_elim; do 2 f_equiv. apply bi.or_intro_l. apply bi.or_intro_r.
 Qed.
 
-Lemma monPred_relatively_sep P Q : ∃ᵢ (P ∗ Q) ⊢ ∃ᵢ P ∗ ∃ᵢ Q.
+Lemma monPred_subjectively_sep P Q : <subj> (P ∗ Q) ⊢ <subj> P ∗ <subj> Q.
 Proof. unseal. split=>i /=. apply bi.exist_elim=>?. by rewrite -!bi.exist_intro. Qed.
 
-Lemma monPred_relatively_idemp P : ∃ᵢ (∃ᵢ P) ⊣⊢ ∃ᵢ P.
+Lemma monPred_subjectively_idemp P : <subj> <subj> P ⊣⊢ <subj> P.
 Proof.
-  apply bi.equiv_spec; split; [|by apply monPred_relatively_intro].
+  apply bi.equiv_spec; split; [|by apply monPred_subjectively_intro].
   unseal. split=>i /=. by apply bi.exist_elim=>_.
 Qed.
 
-Lemma absolute_absolutely P `{!Absolute P} : P ⊢ ∀ᵢ P.
+Lemma objective_objectively P `{!Objective P} : P ⊢ <obj> P.
 Proof.
-  rewrite monPred_absolutely_unfold /= embed_forall. apply bi.forall_intro=>?.
-  split=>?. unseal. apply absolute_at, _.
+  rewrite monPred_objectively_unfold /= embed_forall. apply bi.forall_intro=>?.
+  split=>?. unseal. apply objective_at, _.
 Qed.
-Lemma absolute_relatively P `{!Absolute P} : ∃ᵢ P ⊢ P.
+Lemma objective_subjectively P `{!Objective P} : <subj> P ⊢ P.
 Proof.
-  rewrite monPred_relatively_unfold /= embed_exist. apply bi.exist_elim=>?.
-  split=>?. unseal. apply absolute_at, _.
+  rewrite monPred_subjectively_unfold /= embed_exist. apply bi.exist_elim=>?.
+  split=>?. unseal. apply objective_at, _.
 Qed.
 
-Global Instance embed_absolute (P : PROP) : @Absolute I PROP ⎡P⎤.
+Global Instance embed_objective (P : PROP) : @Objective I PROP ⎡P⎤.
 Proof. intros ??. by unseal. Qed.
-Global Instance pure_absolute φ : @Absolute I PROP ⌜φ⌝.
+Global Instance pure_objective φ : @Objective I PROP ⌜φ⌝.
 Proof. intros ??. by unseal. Qed.
-Global Instance emp_absolute : @Absolute I PROP emp.
+Global Instance emp_objective : @Objective I PROP emp.
 Proof. intros ??. by unseal. Qed.
-Global Instance absolutely_absolute P : Absolute (∀ᵢ P).
+Global Instance objectively_objective P : Objective (<obj> P).
 Proof. intros ??. by unseal. Qed.
-Global Instance relatively_absolute P : Absolute (∃ᵢ P).
+Global Instance subjectively_objective P : Objective (<subj> P).
 Proof. intros ??. by unseal. Qed.
 
-Global Instance and_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∧ Q).
-Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
-Global Instance or_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∨ Q).
-Proof. intros i j. by rewrite !monPred_at_or !(absolute_at _ i j). Qed.
-Global Instance impl_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P → Q).
+Global Instance and_objective P Q `{!Objective P, !Objective Q} : Objective (P ∧ Q).
+Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
+Global Instance or_objective P Q `{!Objective P, !Objective Q} : Objective (P ∨ Q).
+Proof. intros i j. by rewrite !monPred_at_or !(objective_at _ i j). Qed.
+Global Instance impl_objective P Q `{!Objective P, !Objective Q} : Objective (P → Q).
 Proof.
   intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
   rewrite bi.forall_elim //. apply bi.forall_intro=> k.
   rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
-  rewrite (absolute_at Q i). by rewrite (absolute_at P k).
+  rewrite (objective_at Q i). by rewrite (objective_at P k).
 Qed.
-Global Instance forall_absolute {A} Φ {H : ∀ x : A, Absolute (Φ x)} :
-  @Absolute I PROP (∀ x, Φ x)%I.
-Proof. intros i j. unseal. do 2 f_equiv. by apply absolute_at. Qed.
-Global Instance exists_absolute {A} Φ {H : ∀ x : A, Absolute (Φ x)} :
-  @Absolute I PROP (∃ x, Φ x)%I.
-Proof. intros i j. unseal. do 2 f_equiv. by apply absolute_at. Qed.
+Global Instance forall_objective {A} Φ {H : ∀ x : A, Objective (Φ x)} :
+  @Objective I PROP (∀ x, Φ x)%I.
+Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
+Global Instance exists_objective {A} Φ {H : ∀ x : A, Objective (Φ x)} :
+  @Objective I PROP (∃ x, Φ x)%I.
+Proof. intros i j. unseal. do 2 f_equiv. by apply objective_at. Qed.
 
-Global Instance sep_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P ∗ Q).
-Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
-Global Instance wand_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P -∗ Q).
+Global Instance sep_objective P Q `{!Objective P, !Objective Q} : Objective (P ∗ Q).
+Proof. intros i j. unseal. by rewrite !(objective_at _ i j). Qed.
+Global Instance wand_objective P Q `{!Objective P, !Objective Q} : Objective (P -∗ Q).
 Proof.
   intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
   rewrite bi.forall_elim //. apply bi.forall_intro=> k.
   rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
-  rewrite (absolute_at Q i). by rewrite (absolute_at P k).
+  rewrite (objective_at Q i). by rewrite (objective_at P k).
 Qed.
-Global Instance persistently_absolute P `{!Absolute P} :
-  Absolute (bi_persistently P).
-Proof. intros i j. unseal. by rewrite absolute_at. Qed.
+Global Instance persistently_objective P `{!Objective P} : Objective (<pers> P).
+Proof. intros i j. unseal. by rewrite objective_at. Qed.
 
-Global Instance affinely_absolute P `{!Absolute P} : Absolute (bi_affinely P).
+Global Instance affinely_objective P `{!Objective P} : Objective (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
-Global Instance absorbingly_absolute P `{!Absolute P} :
-  Absolute (bi_absorbingly P).
+Global Instance absorbingly_objective P `{!Objective P} : Objective (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
-Global Instance persistently_if_absolute P p `{!Absolute P} :
-  Absolute (bi_persistently_if p P).
+Global Instance persistently_if_objective P p `{!Objective P} : Objective (<pers>?p P).
 Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
-Global Instance affinely_if_absolute P p `{!Absolute P} :
-  Absolute (bi_affinely_if p P).
+Global Instance affinely_if_objective P p `{!Objective P} : Objective (<affine>?p P).
 Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.
 
 (** monPred_in *)
@@ -752,70 +746,70 @@ Lemma monPred_at_big_sepMS `{Countable A} i (Φ : A → monPred) (X : gmultiset
   ([∗ mset] y ∈ X, Φ y) i ⊣⊢ ([∗ mset] y ∈ X, Φ y i).
 Proof. apply (big_opMS_commute (flip monPred_at i)). Qed.
 
-Global Instance monPred_absolutely_monoid_and_homomorphism :
-  MonoidHomomorphism bi_and bi_and (≡) (@monPred_absolutely I PROP).
+Global Instance monPred_objectively_monoid_and_homomorphism :
+  MonoidHomomorphism bi_and bi_and (≡) (@monPred_objectively I PROP).
 Proof.
-  split; [split|]; try apply _. apply monPred_absolutely_and.
-  apply monPred_absolutely_pure.
+  split; [split|]; try apply _. apply monPred_objectively_and.
+  apply monPred_objectively_pure.
 Qed.
-Global Instance monPred_absolutely_monoid_sep_entails_homomorphism :
-  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@monPred_absolutely I PROP).
+Global Instance monPred_objectively_monoid_sep_entails_homomorphism :
+  MonoidHomomorphism bi_sep bi_sep (flip (⊢)) (@monPred_objectively I PROP).
 Proof.
-  split; [split|]; try apply _. apply monPred_absolutely_sep_2.
-  by rewrite monPred_absolutely_emp.
+  split; [split|]; try apply _. apply monPred_objectively_sep_2.
+  by rewrite monPred_objectively_emp.
 Qed.
-Global Instance monPred_absolutely_monoid_sep_homomorphism `{BiIndexBottom bot} :
-  MonoidHomomorphism bi_sep bi_sep (≡) (@monPred_absolutely I PROP).
+Global Instance monPred_objectively_monoid_sep_homomorphism `{BiIndexBottom bot} :
+  MonoidHomomorphism bi_sep bi_sep (≡) (@monPred_objectively I PROP).
 Proof.
-  split; [split|]; try apply _. apply monPred_absolutely_sep.
-  by rewrite monPred_absolutely_emp.
+  split; [split|]; try apply _. apply monPred_objectively_sep.
+  by rewrite monPred_objectively_emp.
 Qed.
 
-Lemma monPred_absolutely_big_sepL_entails {A} (Φ : nat → A → monPred) l :
-  ([∗ list] k↦x ∈ l, ∀ᵢ (Φ k x)) ⊢ ∀ᵢ ([∗ list] k↦x ∈ l, Φ k x).
-Proof. apply (big_opL_commute monPred_absolutely (R:=flip (⊢))). Qed.
-Lemma monPred_absolutely_big_sepM_entails
+Lemma monPred_objectively_big_sepL_entails {A} (Φ : nat → A → monPred) l :
+  ([∗ list] k↦x ∈ l, <obj> (Φ k x)) ⊢ <obj> ([∗ list] k↦x ∈ l, Φ k x).
+Proof. apply (big_opL_commute monPred_objectively (R:=flip (⊢))). Qed.
+Lemma monPred_objectively_big_sepM_entails
       `{Countable K} {A} (Φ : K → A → monPred) (m : gmap K A) :
-  ([∗ map] k↦x ∈ m, ∀ᵢ (Φ k x)) ⊢ ∀ᵢ ([∗ map] k↦x ∈ m, Φ k x).
-Proof. apply (big_opM_commute monPred_absolutely (R:=flip (⊢))). Qed.
-Lemma monPred_absolutely_big_sepS_entails `{Countable A} (Φ : A → monPred) (X : gset A) :
-  ([∗ set] y ∈ X, ∀ᵢ (Φ y)) ⊢ ∀ᵢ ([∗ set] y ∈ X, Φ y).
-Proof. apply (big_opS_commute monPred_absolutely (R:=flip (⊢))). Qed.
-Lemma monPred_absolutely_big_sepMS_entails `{Countable A} (Φ : A → monPred) (X : gmultiset A) :
-  ([∗ mset] y ∈ X, ∀ᵢ (Φ y)) ⊢ ∀ᵢ ([∗ mset] y ∈ X, Φ y).
-Proof. apply (big_opMS_commute monPred_absolutely (R:=flip (⊢))). Qed.
-
-Lemma monPred_absolutely_big_sepL `{BiIndexBottom bot} {A} (Φ : nat → A → monPred) l :
-  ∀ᵢ ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, ∀ᵢ (Φ k x)).
+  ([∗ map] k↦x ∈ m, <obj> (Φ k x)) ⊢ <obj> ([∗ map] k↦x ∈ m, Φ k x).
+Proof. apply (big_opM_commute monPred_objectively (R:=flip (⊢))). Qed.
+Lemma monPred_objectively_big_sepS_entails `{Countable A} (Φ : A → monPred) (X : gset A) :
+  ([∗ set] y ∈ X, <obj> (Φ y)) ⊢ <obj> ([∗ set] y ∈ X, Φ y).
+Proof. apply (big_opS_commute monPred_objectively (R:=flip (⊢))). Qed.
+Lemma monPred_objectively_big_sepMS_entails `{Countable A} (Φ : A → monPred) (X : gmultiset A) :
+  ([∗ mset] y ∈ X, <obj> (Φ y)) ⊢ <obj> ([∗ mset] y ∈ X, Φ y).
+Proof. apply (big_opMS_commute monPred_objectively (R:=flip (⊢))). Qed.
+
+Lemma monPred_objectively_big_sepL `{BiIndexBottom bot} {A} (Φ : nat → A → monPred) l :
+  <obj> ([∗ list] k↦x ∈ l, Φ k x) ⊣⊢ ([∗ list] k↦x ∈ l, <obj> (Φ k x)).
 Proof. apply (big_opL_commute _). Qed.
-Lemma monPred_absolutely_big_sepM `{BiIndexBottom bot} `{Countable K} {A}
+Lemma monPred_objectively_big_sepM `{BiIndexBottom bot} `{Countable K} {A}
       (Φ : K → A → monPred) (m : gmap K A) :
-  ∀ᵢ ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, ∀ᵢ (Φ k x)).
+  <obj> ([∗ map] k↦x ∈ m, Φ k x) ⊣⊢ ([∗ map] k↦x ∈ m, <obj> (Φ k x)).
 Proof. apply (big_opM_commute _). Qed.
-Lemma monPred_absolutely_big_sepS `{BiIndexBottom bot} `{Countable A}
+Lemma monPred_objectively_big_sepS `{BiIndexBottom bot} `{Countable A}
       (Φ : A → monPred) (X : gset A) :
-  ∀ᵢ ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ∀ᵢ (Φ y)).
+  <obj> ([∗ set] y ∈ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, <obj> (Φ y)).
 Proof. apply (big_opS_commute _). Qed.
-Lemma monPred_absolutely_big_sepMS `{BiIndexBottom bot} `{Countable A}
+Lemma monPred_objectively_big_sepMS `{BiIndexBottom bot} `{Countable A}
       (Φ : A → monPred) (X : gmultiset A) :
-  ∀ᵢ ([∗ mset] y ∈ X, Φ y) ⊣⊢  ([∗ mset] y ∈ X, ∀ᵢ (Φ y)).
+  <obj> ([∗ mset] y ∈ X, Φ y) ⊣⊢  ([∗ mset] y ∈ X, <obj> (Φ y)).
 Proof. apply (big_opMS_commute _). Qed.
 
-Global Instance big_sepL_absolute {A} (l : list A) Φ `{∀ n x, Absolute (Φ n x)} :
-  @Absolute I PROP ([∗ list] n↦x ∈ l, Φ n x)%I.
+Global Instance big_sepL_objective {A} (l : list A) Φ `{∀ n x, Objective (Φ n x)} :
+  @Objective I PROP ([∗ list] n↦x ∈ l, Φ n x)%I.
 Proof. generalize dependent Φ. induction l=>/=; apply _. Qed.
-Global Instance big_sepM_absolute `{Countable K} {A}
-       (Φ : K → A → monPred) (m : gmap K A) `{∀ k x, Absolute (Φ k x)} :
-  Absolute ([∗ map] k↦x ∈ m, Φ k x)%I.
-Proof. intros ??. rewrite !monPred_at_big_sepM. do 3 f_equiv. by apply absolute_at. Qed.
-Global Instance big_sepS_absolute `{Countable A} (Φ : A → monPred)
-       (X : gset A) `{∀ y, Absolute (Φ y)} :
-  Absolute ([∗ set] y ∈ X, Φ y)%I.
-Proof. intros ??. rewrite !monPred_at_big_sepS. do 2 f_equiv. by apply absolute_at. Qed.
-Global Instance big_sepMS_absolute `{Countable A} (Φ : A → monPred)
-       (X : gmultiset A) `{∀ y, Absolute (Φ y)} :
-  Absolute ([∗ mset] y ∈ X, Φ y)%I.
-Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply absolute_at. Qed.
+Global Instance big_sepM_objective `{Countable K} {A}
+       (Φ : K → A → monPred) (m : gmap K A) `{∀ k x, Objective (Φ k x)} :
+  Objective ([∗ map] k↦x ∈ m, Φ k x)%I.
+Proof. intros ??. rewrite !monPred_at_big_sepM. do 3 f_equiv. by apply objective_at. Qed.
+Global Instance big_sepS_objective `{Countable A} (Φ : A → monPred)
+       (X : gset A) `{∀ y, Objective (Φ y)} :
+  Objective ([∗ set] y ∈ X, Φ y)%I.
+Proof. intros ??. rewrite !monPred_at_big_sepS. do 2 f_equiv. by apply objective_at. Qed.
+Global Instance big_sepMS_objective `{Countable A} (Φ : A → monPred)
+       (X : gmultiset A) `{∀ y, Objective (Φ y)} :
+  Objective ([∗ mset] y ∈ X, Φ y)%I.
+Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objective_at. Qed.
 
 (** bupd *)
 Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
@@ -841,9 +835,9 @@ Proof.
   - rewrite !bi.forall_elim //.
   - do 2 apply bi.forall_intro=>?. by do 2 f_equiv.
 Qed.
-Global Instance bupd_absolute `{BiBUpd PROP} P `{!Absolute P} :
-  Absolute (|==> P)%I.
-Proof. intros ??. by rewrite !monPred_at_bupd absolute_at. Qed.
+Global Instance bupd_objective `{BiBUpd PROP} P `{!Objective P} :
+  Objective (|==> P)%I.
+Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
 
 Global Instance monPred_bi_embed_bupd `{BiBUpd PROP} :
   BiEmbedBUpd PROP monPredI.
@@ -866,12 +860,12 @@ Global Instance monPred_at_timeless P i : Timeless P → Timeless (P i).
 Proof. move => [] /(_ i). unfold Timeless. by unseal. Qed.
 Global Instance monPred_in_timeless i0 : Timeless (@monPred_in I PROP i0).
 Proof. split => ? /=. unseal. apply timeless, _. Qed.
-Global Instance monPred_absolutely_timeless P : Timeless P → Timeless (∀ᵢ P).
+Global Instance monPred_objectively_timeless P : Timeless P → Timeless (<obj> P).
 Proof.
   move=>[]. unfold Timeless. unseal=>Hti. split=> ? /=.
   by apply timeless, bi.forall_timeless.
 Qed.
-Global Instance monPred_relatively_timeless P : Timeless P → Timeless (∃ᵢ P).
+Global Instance monPred_subjectively_timeless P : Timeless P → Timeless (<subj> P).
 Proof.
   move=>[]. unfold Timeless. unseal=>Hti. split=> ? /=.
   by apply timeless, bi.exist_timeless.
@@ -973,30 +967,30 @@ Proof.
                -bi.f_equiv -bi.sig_equivI !bi.ofe_fun_equivI.
 Qed.
 
-Global Instance monPred_absolutely_plain `{BiPlainly PROP} P : Plain P → Plain (∀ᵢ P).
-Proof. rewrite monPred_absolutely_unfold. apply _. Qed.
-Global Instance monPred_relatively_plain `{BiPlainly PROP} P : Plain P → Plain (∃ᵢ P).
-Proof. rewrite monPred_relatively_unfold. apply _. Qed.
+Global Instance monPred_objectively_plain `{BiPlainly PROP} P : Plain P → Plain (<obj> P).
+Proof. rewrite monPred_objectively_unfold. apply _. Qed.
+Global Instance monPred_subjectively_plain `{BiPlainly PROP} P : Plain P → Plain (<subj> P).
+Proof. rewrite monPred_subjectively_unfold. apply _. Qed.
 
-(** Absolute  *)
-Global Instance plainly_absolute `{BiPlainly PROP} P : Absolute (â–  P).
+(** Objective  *)
+Global Instance plainly_objective `{BiPlainly PROP} P : Objective (â–  P).
 Proof. intros ??. by unseal. Qed.
-Global Instance plainly_if_absolute `{BiPlainly PROP} P p `{!Absolute P} :
-  Absolute (â– ?p P).
+Global Instance plainly_if_objective `{BiPlainly PROP} P p `{!Objective P} :
+  Objective (â– ?p P).
 Proof. rewrite /plainly_if. destruct p; apply _. Qed.
 
-Global Instance internal_eq_absolute {A : ofeT} (x y : A) :
-  @Absolute I PROP (x ≡ y)%I.
+Global Instance internal_eq_objective {A : ofeT} (x y : A) :
+  @Objective I PROP (x ≡ y)%I.
 Proof. intros ??. by unseal. Qed.
 
-Global Instance later_absolute P `{!Absolute P} : Absolute (â–· P)%I.
-Proof. intros ??. unseal. by rewrite absolute_at. Qed.
-Global Instance laterN_absolute P `{!Absolute P} n : Absolute (â–·^n P)%I.
+Global Instance later_objective P `{!Objective P} : Objective (â–· P)%I.
+Proof. intros ??. unseal. by rewrite objective_at. Qed.
+Global Instance laterN_objective P `{!Objective P} n : Objective (â–·^n P)%I.
 Proof. induction n; apply _. Qed.
-Global Instance except0_absolute P `{!Absolute P} : Absolute (â—‡ P)%I.
+Global Instance except0_objective P `{!Objective P} : Objective (â—‡ P)%I.
 Proof. rewrite /sbi_except_0. apply _. Qed.
 
-Global Instance fupd_absolute E1 E2 P `{!Absolute P} `{BiFUpd PROP} :
-  Absolute (|={E1,E2}=> P)%I.
-Proof. intros ??. by rewrite !monPred_at_fupd absolute_at. Qed.
+Global Instance fupd_objective E1 E2 P `{!Objective P} `{BiFUpd PROP} :
+  Objective (|={E1,E2}=> P)%I.
+Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
 End sbi_facts.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index a3c7d83fb29c0a825198a456711320e0683504b4..7f63cc8bf3b77276d19f8575b44c5c78ad89cb86 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -13,7 +13,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
   bi_plainly_mixin_plainly_ne : NonExpansive plainly;
 
   bi_plainly_mixin_plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q;
-  bi_plainly_mixin_plainly_elim_persistently P : ■ P ⊢ bi_persistently P;
+  bi_plainly_mixin_plainly_elim_persistently P : ■ P ⊢ <pers> P;
   bi_plainly_mixin_plainly_idemp_2 P : ■ P ⊢ ■ ■ P;
 
   bi_plainly_mixin_plainly_forall_2 {A} (Ψ : A → PROP) :
@@ -23,7 +23,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
      for persistently and plainly, but for any modality defined as `M P n x :=
      ∀ y, R x y → P n y`. *)
   bi_plainly_mixin_persistently_impl_plainly P Q :
-    (■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q);
+    (■ P → <pers> Q) ⊢ <pers> (■ P → Q);
   bi_plainly_mixin_plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q);
 
   bi_plainly_mixin_plainly_emp_intro P : P ⊢ ■ emp;
@@ -59,14 +59,13 @@ Section plainly_laws.
 
   Lemma plainly_mono P Q : (P ⊢ Q) → ■ P ⊢ ■ Q.
   Proof. eapply bi_plainly_mixin_plainly_mono, bi_plainly_mixin. Qed.
-  Lemma plainly_elim_persistently P : ■ P ⊢ bi_persistently P.
+  Lemma plainly_elim_persistently P : ■ P ⊢ <pers> P.
   Proof. eapply bi_plainly_mixin_plainly_elim_persistently, bi_plainly_mixin. Qed.
   Lemma plainly_idemp_2 P : ■ P ⊢ ■ ■ P.
   Proof. eapply bi_plainly_mixin_plainly_idemp_2, bi_plainly_mixin. Qed.
   Lemma plainly_forall_2 {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a).
   Proof. eapply bi_plainly_mixin_plainly_forall_2, bi_plainly_mixin. Qed.
-  Lemma persistently_impl_plainly P Q :
-    (■ P → bi_persistently Q) ⊢ bi_persistently (■ P → Q).
+  Lemma persistently_impl_plainly P Q : (■ P → <pers> Q) ⊢ <pers> (■ P → Q).
   Proof. eapply bi_plainly_mixin_persistently_impl_plainly, bi_plainly_mixin. Qed.
   Lemma plainly_impl_plainly P Q : (■ P → ■ Q) ⊢ ■ (■ P → Q).
   Proof. eapply bi_plainly_mixin_plainly_impl_plainly, bi_plainly_mixin. Qed.
@@ -119,19 +118,19 @@ Global Instance plainly_flip_mono' :
   Proper (flip (⊢) ==> flip (⊢)) (@plainly PROP _).
 Proof. intros P Q; apply plainly_mono. Qed.
 
-Lemma affinely_plainly_elim P : bi_affinely (■ P) ⊢ P.
+Lemma affinely_plainly_elim P : <affine> ■ P ⊢ P.
 Proof. by rewrite plainly_elim_persistently affinely_persistently_elim. Qed.
 
-Lemma persistently_plainly P : bi_persistently (■ P) ⊣⊢ ■ P.
+Lemma persistently_plainly P : <pers> ■ P ⊣⊢ ■ P.
 Proof.
   apply (anti_symm _).
   - by rewrite persistently_elim_absorbingly /bi_absorbingly comm plainly_absorb.
   - by rewrite {1}plainly_idemp_2 plainly_elim_persistently.
 Qed.
-Lemma persistently_if_plainly P p : bi_persistently_if p (■ P) ⊣⊢ ■ P.
+Lemma persistently_if_plainly P p : <pers>?p ■ P ⊣⊢ ■ P.
 Proof. destruct p; last done. exact: persistently_plainly. Qed.
 
-Lemma plainly_persistently P : ■ (bi_persistently P) ⊣⊢ ■ P.
+Lemma plainly_persistently P : ■ <pers> P ⊣⊢ ■ P.
 Proof.
   apply (anti_symm _).
   - rewrite -{1}(left_id True%I bi_and (â–  _)%I) (plainly_emp_intro True%I).
@@ -140,7 +139,7 @@ Proof.
   - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
 Qed.
 
-Lemma absorbingly_plainly P : bi_absorbingly (■ P) ⊣⊢ ■ P.
+Lemma absorbingly_plainly P : <absorb> ■ P ⊣⊢ ■ P.
 Proof. by rewrite -(persistently_plainly P) absorbingly_persistently. Qed.
 
 Lemma plainly_and_sep_elim P Q : ■ P ∧ Q -∗ (emp ∧ P) ∗ Q.
@@ -149,7 +148,7 @@ Lemma plainly_and_sep_assoc P Q R : ■ P ∧ (Q ∗ R) ⊣⊢ (■ P ∧ Q) ∗
 Proof. by rewrite -(persistently_plainly P) persistently_and_sep_assoc. Qed.
 Lemma plainly_and_emp_elim P : emp ∧ ■ P ⊢ P.
 Proof. by rewrite plainly_elim_persistently persistently_and_emp_elim. Qed.
-Lemma plainly_elim_absorbingly P : ■ P ⊢ bi_absorbingly P.
+Lemma plainly_elim_absorbingly P : ■ P ⊢ <absorb> P.
 Proof. by rewrite plainly_elim_persistently persistently_elim_absorbingly. Qed.
 Lemma plainly_elim P `{!Absorbing P} : ■ P ⊢ P.
 Proof. by rewrite plainly_elim_persistently persistently_elim. Qed.
@@ -214,7 +213,7 @@ Proof.
   by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
 Qed.
 
-Lemma plainly_affinely P : ■ (bi_affinely P) ⊣⊢ ■ P.
+Lemma plainly_affinely P : ■ <affine> P ⊣⊢ ■ P.
 Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
 
 Lemma and_sep_plainly P Q : ■ P ∧ ■ Q ⊣⊢ ■ P ∗ ■ Q.
@@ -252,7 +251,7 @@ Qed.
 Lemma impl_wand_plainly_2 P Q : (■ P -∗ Q) ⊢ (■ P → Q).
 Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
 
-Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (bi_affinely (■ P) -∗ Q).
+Lemma impl_wand_affinely_plainly P Q : (■ P → Q) ⊣⊢ (<affine> ■ P -∗ Q).
 Proof. by rewrite -(persistently_plainly P) impl_wand_affinely_persistently. Qed.
 
 Section plainly_affine_bi.
@@ -351,7 +350,7 @@ Proof. by rewrite /Persistent persistently_plainly. Qed.
 Global Instance wand_persistent P Q :
   Plain P → Persistent Q → Absorbing Q → Persistent (P -∗ Q).
 Proof.
-  intros. rewrite /Persistent {2}(plain P). trans (bi_persistently (■ P → Q)%I).
+  intros. rewrite /Persistent {2}(plain P). trans (<pers> (■ P → Q))%I.
   - rewrite -persistently_impl_plainly impl_wand_affinely_plainly -(persistent Q).
     by rewrite affinely_plainly_elim.
   - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
@@ -428,13 +427,13 @@ Proof. intros. by rewrite /Plain -plainly_sep_2 -!plain. Qed.
 
 Global Instance plainly_plain P : Plain (â–  P).
 Proof. by rewrite /Plain plainly_idemp. Qed.
-Global Instance persistently_plain P : Plain P → Plain (bi_persistently P).
+Global Instance persistently_plain P : Plain P → Plain (<pers> P).
 Proof.
   rewrite /Plain=> HP. rewrite {1}HP plainly_persistently persistently_plainly //.
 Qed.
-Global Instance affinely_plain P : Plain P → Plain (bi_affinely P).
+Global Instance affinely_plain P : Plain P → Plain (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
-Global Instance absorbingly_plain P : Plain P → Plain (bi_absorbingly P).
+Global Instance absorbingly_plain P : Plain P → Plain (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 Global Instance from_option_plain {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Plain (Ψ x)) → Plain P → Plain (from_option Ψ P mx).
@@ -449,7 +448,7 @@ Proof.
   rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
 Qed.
 
-Lemma plainly_alt P : ■ P ⊣⊢ bi_affinely P ≡ emp.
+Lemma plainly_alt P : ■ P ⊣⊢ <affine> P ≡ emp.
 Proof.
   rewrite -plainly_affinely. apply (anti_symm (⊢)).
   - rewrite -prop_ext. apply plainly_mono, and_intro; apply wand_intro_l.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 2cd2a6f3e7e08a0222fef8a28b29305e3d46e24c..84954fee1e19ef624e1dd81222b2342ca3cf467f 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -17,7 +17,7 @@ Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
     state_interp σ1 ={⊤}=∗ state_interp σ2 ∗ twptp t2)%I.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
-  ((bi_persistently (∀ t, twptp1 t -∗ twptp2 t)) →
+  (<pers> (∀ t, twptp1 t -∗ twptp2 t) →
   ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t)%I.
 Proof.
   iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 4a3ab703ff7e18a40691abd0235f2a4f7e813ec2..e364691465c56163a2ed12101af20203e16c8ad0 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -11,7 +11,7 @@ Implicit Types P Q R : PROP.
 (* FromAffinely *)
 Global Instance from_affinely_affine P : Affine P → FromAffinely P P.
 Proof. intros. by rewrite /FromAffinely affinely_elim. Qed.
-Global Instance from_affinely_default P : FromAffinely (bi_affinely P) P | 100.
+Global Instance from_affinely_default P : FromAffinely (<affine> P) P | 100.
 Proof. by rewrite /FromAffinely. Qed.
 
 (* IntoAbsorbingly *)
@@ -19,7 +19,7 @@ Global Instance into_absorbingly_True : @IntoAbsorbingly PROP True emp | 0.
 Proof. by rewrite /IntoAbsorbingly -absorbingly_True_emp absorbingly_pure. Qed.
 Global Instance into_absorbingly_absorbing P : Absorbing P → IntoAbsorbingly P P | 1.
 Proof. intros. by rewrite /IntoAbsorbingly absorbing_absorbingly. Qed.
-Global Instance into_absorbingly_default P : IntoAbsorbingly (bi_absorbingly P) P | 100.
+Global Instance into_absorbingly_default P : IntoAbsorbingly (<absorb> P) P | 100.
 Proof. by rewrite /IntoAbsorbingly. Qed.
 
 (* FromAssumption *)
@@ -27,19 +27,19 @@ Global Instance from_assumption_exact p P : FromAssumption p P P | 0.
 Proof. by rewrite /FromAssumption /= affinely_persistently_if_elim. Qed.
 
 Global Instance from_assumption_persistently_r P Q :
-  FromAssumption true P Q → KnownRFromAssumption true P (bi_persistently Q).
+  FromAssumption true P Q → KnownRFromAssumption true P (<pers> Q).
 Proof.
   rewrite /KnownRFromAssumption /FromAssumption /= =><-.
   by rewrite -{1}affinely_persistently_idemp affinely_elim.
 Qed.
 Global Instance from_assumption_affinely_r P Q :
-  FromAssumption true P Q → KnownRFromAssumption true P (bi_affinely Q).
+  FromAssumption true P Q → KnownRFromAssumption true P (<affine> Q).
 Proof.
   rewrite /KnownRFromAssumption /FromAssumption /= =><-.
   by rewrite affinely_idemp.
 Qed.
 Global Instance from_assumption_absorbingly_r p P Q :
-  FromAssumption p P Q → KnownRFromAssumption p P (bi_absorbingly Q).
+  FromAssumption p P Q → KnownRFromAssumption p P (<absorb> Q).
 Proof.
   rewrite /KnownRFromAssumption /FromAssumption /= =><-.
   apply absorbingly_intro.
@@ -52,19 +52,19 @@ Proof.
   by rewrite affinely_persistently_if_elim.
 Qed.
 Global Instance from_assumption_persistently_l_true P Q :
-  FromAssumption true P Q → KnownLFromAssumption true (bi_persistently P) Q.
+  FromAssumption true P Q → KnownLFromAssumption true (<pers> P) Q.
 Proof.
   rewrite /KnownLFromAssumption /FromAssumption /= =><-.
   by rewrite persistently_idemp.
 Qed.
 Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
-  FromAssumption true P Q → KnownLFromAssumption false (bi_persistently P) Q.
+  FromAssumption true P Q → KnownLFromAssumption false (<pers> P) Q.
 Proof.
   rewrite /KnownLFromAssumption /FromAssumption /= =><-.
   by rewrite affine_affinely.
 Qed.
 Global Instance from_assumption_affinely_l_true p P Q :
-  FromAssumption p P Q → KnownLFromAssumption p (bi_affinely P) Q.
+  FromAssumption p P Q → KnownLFromAssumption p (<affine> P) Q.
 Proof.
   rewrite /KnownLFromAssumption /FromAssumption /= =><-.
   by rewrite affinely_elim.
@@ -110,13 +110,12 @@ Proof.
           bi.wand_elim_r absorbing //.
 Qed.
 
-Global Instance into_pure_affinely P φ :
-  IntoPure P φ → IntoPure (bi_affinely P) φ.
+Global Instance into_pure_affinely P φ : IntoPure P φ → IntoPure (<affine> P) φ.
 Proof. rewrite /IntoPure=> ->. apply affinely_elim. Qed.
-Global Instance into_pure_absorbingly P φ : IntoPure P φ → IntoPure (bi_absorbingly P) φ.
+Global Instance into_pure_absorbingly P φ : IntoPure P φ → IntoPure (<absorb> P) φ.
 Proof. rewrite /IntoPure=> ->. by rewrite absorbingly_pure. Qed.
 Global Instance into_pure_persistently P φ :
-  IntoPure P φ → IntoPure (bi_persistently P) φ.
+  IntoPure P φ → IntoPure (<pers> P) φ.
 Proof. rewrite /IntoPure=> ->. apply: persistently_elim. Qed.
 Global Instance into_pure_embed `{BiEmbed PROP PROP'} P φ :
   IntoPure P φ → IntoPure ⎡P⎤ φ.
@@ -175,20 +174,19 @@ Proof.
 Qed.
 
 Global Instance from_pure_persistently P a φ :
-  FromPure true P φ → FromPure a (bi_persistently P) φ.
+  FromPure true P φ → FromPure a (<pers> P) φ.
 Proof.
   rewrite /FromPure=> <- /=.
   by rewrite persistently_affinely affinely_if_elim persistently_pure.
 Qed.
 Global Instance from_pure_affinely_true P φ :
-  FromPure true P φ → FromPure true (bi_affinely P) φ.
+  FromPure true P φ → FromPure true (<affine> P) φ.
 Proof. rewrite /FromPure=><- /=. by rewrite affinely_idemp. Qed.
 Global Instance from_pure_affinely_false P φ `{!Affine P} :
-  FromPure false P φ → FromPure false (bi_affinely P) φ.
+  FromPure false P φ → FromPure false (<affine> P) φ.
 Proof. rewrite /FromPure /= affine_affinely //. Qed.
 
-Global Instance from_pure_absorbingly P φ :
-  FromPure true P φ → FromPure false (bi_absorbingly P) φ.
+Global Instance from_pure_absorbingly P φ : FromPure true P φ → FromPure false (<absorb> P) φ.
 Proof. rewrite /FromPure=> <- /=. apply persistent_absorbingly_affinely, _. Qed.
 Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
   FromPure a P φ → FromPure a ⎡P⎤ φ.
@@ -196,13 +194,13 @@ Proof. rewrite /FromPure=> <-. by rewrite embed_affinely_if embed_pure. Qed.
 
 (* IntoPersistent *)
 Global Instance into_persistent_persistently p P Q :
-  IntoPersistent true P Q → IntoPersistent p (bi_persistently P) Q | 0.
+  IntoPersistent true P Q → IntoPersistent p (<pers> P) Q | 0.
 Proof.
   rewrite /IntoPersistent /= => ->.
   destruct p; simpl; auto using persistently_idemp_1.
 Qed.
 Global Instance into_persistent_affinely p P Q :
-  IntoPersistent p P Q → IntoPersistent p (bi_affinely P) Q | 0.
+  IntoPersistent p P Q → IntoPersistent p (<affine> P) Q | 0.
 Proof. rewrite /IntoPersistent /= => <-. by rewrite affinely_elim. Qed.
 Global Instance into_persistent_embed `{BiEmbed PROP PROP'} p P Q :
   IntoPersistent p P Q → IntoPersistent p ⎡P⎤ ⎡Q⎤ | 0.
@@ -217,11 +215,11 @@ Proof. intros. by rewrite /IntoPersistent. Qed.
 
 (* FromModal *)
 Global Instance from_modal_affinely P :
-  FromModal modality_affinely (bi_affinely P) (bi_affinely P) P | 2.
+  FromModal modality_affinely (<affine> P) (<affine> P) P | 2.
 Proof. by rewrite /FromModal. Qed.
 
 Global Instance from_modal_persistently P :
-  FromModal modality_persistently (bi_persistently P) (bi_persistently P) P | 2.
+  FromModal modality_persistently (<pers> P) (<pers> P) P | 2.
 Proof. by rewrite /FromModal. Qed.
 Global Instance from_modal_affinely_persistently P :
   FromModal modality_affinely_persistently (â–¡ P) (â–¡ P) P | 1.
@@ -231,7 +229,7 @@ Global Instance from_modal_affinely_persistently_affine_bi P :
 Proof. intros. by rewrite /FromModal /= affine_affinely. Qed.
 
 Global Instance from_modal_absorbingly P :
-  FromModal modality_id (bi_absorbingly P) (bi_absorbingly P) P.
+  FromModal modality_id (<absorb> P) (<absorb> P) P.
 Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
 
 (* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
@@ -326,10 +324,10 @@ Global Instance into_wand_affinely_persistently p q R P Q :
   IntoWand p q R P Q → IntoWand p q (□ R) P Q.
 Proof. by rewrite /IntoWand affinely_persistently_elim. Qed.
 Global Instance into_wand_persistently_true q R P Q :
-  IntoWand true q R P Q → IntoWand true q (bi_persistently R) P Q.
+  IntoWand true q R P Q → IntoWand true q (<pers> R) P Q.
 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.
+  IntoWand false q R P Q → IntoWand false q (<pers> R) P Q.
 Proof. by rewrite /IntoWand persistently_elim. Qed.
 Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q :
   IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
@@ -376,11 +374,11 @@ Proof. by rewrite /FromAnd pure_and. Qed.
 
 Global Instance from_and_persistently P Q1 Q2 :
   FromAnd P Q1 Q2 →
-  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
+  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof. rewrite /FromAnd=> <-. by rewrite persistently_and. Qed.
 Global Instance from_and_persistently_sep P Q1 Q2 :
   FromSep P Q1 Q2 →
-  FromAnd (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2) | 11.
+  FromAnd (<pers> P) (<pers> Q1) (<pers> Q2) | 11.
 Proof. rewrite /FromAnd=> <-. by rewrite -persistently_and persistently_and_sep. Qed.
 
 Global Instance from_and_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
@@ -409,14 +407,14 @@ Global Instance from_sep_pure φ ψ : @FromSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜
 Proof. by rewrite /FromSep pure_and sep_and. Qed.
 
 Global Instance from_sep_affinely P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
+  FromSep P Q1 Q2 → FromSep (<affine> P) (<affine> Q1) (<affine> Q2).
 Proof. rewrite /FromSep=> <-. by rewrite affinely_sep_2. Qed.
 Global Instance from_sep_absorbingly P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
+  FromSep P Q1 Q2 → FromSep (<absorb> P) (<absorb> Q1) (<absorb> Q2).
 Proof. rewrite /FromSep=> <-. by rewrite absorbingly_sep. Qed.
 Global Instance from_sep_persistently P Q1 Q2 :
   FromSep P Q1 Q2 →
-  FromSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
+  FromSep (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof. rewrite /FromSep=> <-. by rewrite persistently_sep_2. Qed.
 
 Global Instance from_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
@@ -460,7 +458,7 @@ Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝
 Proof. by rewrite /IntoAnd pure_and affinely_persistently_if_and. Qed.
 
 Global Instance into_and_affinely p P Q1 Q2 :
-  IntoAnd p P Q1 Q2 → IntoAnd p (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
+  IntoAnd p P Q1 Q2 → IntoAnd p (<affine> P) (<affine> Q1) (<affine> Q2).
 Proof.
   rewrite /IntoAnd. destruct p; simpl.
   - by rewrite -affinely_and !persistently_affinely.
@@ -468,7 +466,7 @@ Proof.
 Qed.
 Global Instance into_and_persistently p P Q1 Q2 :
   IntoAnd p P Q1 Q2 →
-  IntoAnd p (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
+  IntoAnd p (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof.
   rewrite /IntoAnd /=. destruct p; simpl.
   - by rewrite -persistently_and !persistently_idemp.
@@ -487,7 +485,7 @@ Proof. by rewrite /IntoSep. Qed.
 
 Inductive AndIntoSep : PROP → PROP → PROP → PROP → Prop :=
   | and_into_sep_affine P Q Q' : Affine P → FromAffinely Q' Q → AndIntoSep P P Q Q'
-  | and_into_sep P Q : AndIntoSep P (bi_affinely P)%I Q Q.
+  | and_into_sep P Q : AndIntoSep P (<affine> P)%I Q Q.
 Existing Class AndIntoSep.
 Global Existing Instance and_into_sep_affine | 0.
 Global Existing Instance and_into_sep | 2.
@@ -517,23 +515,23 @@ Global Instance into_sep_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
 Proof. rewrite /IntoSep -embed_sep=> -> //. Qed.
 
 Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
-  IntoSep P Q1 Q2 → IntoSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2) | 0.
+  IntoSep P Q1 Q2 → IntoSep (<affine> P) (<affine> Q1) (<affine> Q2) | 0.
 Proof. rewrite /IntoSep /= => ->. by rewrite affinely_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_trim P Q1 Q2 :
-  IntoSep P Q1 Q2 → IntoSep (bi_affinely P) Q1 Q2 | 20.
+  IntoSep P Q1 Q2 → IntoSep (<affine> P) Q1 Q2 | 20.
 Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
 
 Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 →
-  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
+  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
 Global Instance into_sep_persistently_affine P Q1 Q2 :
   IntoSep P Q1 Q2 →
   TCOr (Affine Q1) (Absorbing Q2) → TCOr (Absorbing Q1) (Affine Q2) →
-  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
+  IntoSep (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof.
   rewrite /IntoSep /= => -> ??.
   by rewrite sep_and persistently_and persistently_and_sep_l_1.
@@ -567,14 +565,14 @@ Proof. by rewrite /FromOr. Qed.
 Global Instance from_or_pure φ ψ : @FromOr PROP ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /FromOr pure_or. Qed.
 Global Instance from_or_affinely P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
+  FromOr P Q1 Q2 → FromOr (<affine> P) (<affine> Q1) (<affine> Q2).
 Proof. rewrite /FromOr=> <-. by rewrite affinely_or. Qed.
 Global Instance from_or_absorbingly P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
+  FromOr P Q1 Q2 → FromOr (<absorb> P) (<absorb> Q1) (<absorb> Q2).
 Proof. rewrite /FromOr=> <-. by rewrite absorbingly_or. Qed.
 Global Instance from_or_persistently P Q1 Q2 :
   FromOr P Q1 Q2 →
-  FromOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
+  FromOr (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof. rewrite /FromOr=> <-. by rewrite persistently_or. Qed.
 Global Instance from_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   FromOr P Q1 Q2 → FromOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
@@ -586,14 +584,14 @@ Proof. by rewrite /IntoOr. Qed.
 Global Instance into_or_pure φ ψ : @IntoOr PROP ⌜φ ∨ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoOr pure_or. Qed.
 Global Instance into_or_affinely P Q1 Q2 :
-  IntoOr P Q1 Q2 → IntoOr (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2).
+  IntoOr P Q1 Q2 → IntoOr (<affine> P) (<affine> Q1) (<affine> Q2).
 Proof. rewrite /IntoOr=>->. by rewrite affinely_or. Qed.
 Global Instance into_or_absorbingly P Q1 Q2 :
-  IntoOr P Q1 Q2 → IntoOr (bi_absorbingly P) (bi_absorbingly Q1) (bi_absorbingly Q2).
+  IntoOr P Q1 Q2 → IntoOr (<absorb> P) (<absorb> Q1) (<absorb> Q2).
 Proof. rewrite /IntoOr=>->. by rewrite absorbingly_or. Qed.
 Global Instance into_or_persistently P Q1 Q2 :
   IntoOr P Q1 Q2 →
-  IntoOr (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
+  IntoOr (<pers> P) (<pers> Q1) (<pers> Q2).
 Proof. rewrite /IntoOr=>->. by rewrite persistently_or. Qed.
 Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   IntoOr P Q1 Q2 → IntoOr ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
@@ -606,13 +604,13 @@ Global Instance from_exist_pure {A} (φ : A → Prop) :
   @FromExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /FromExist pure_exist. Qed.
 Global Instance from_exist_affinely {A} P (Φ : A → PROP) :
-  FromExist P Φ → FromExist (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
+  FromExist P Φ → FromExist (<affine> P) (λ a, <affine> (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite affinely_exist. Qed.
 Global Instance from_exist_absorbingly {A} P (Φ : A → PROP) :
-  FromExist P Φ → FromExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
+  FromExist P Φ → FromExist (<absorb> P) (λ a, <absorb> (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite absorbingly_exist. Qed.
 Global Instance from_exist_persistently {A} P (Φ : A → PROP) :
-  FromExist P Φ → FromExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
+  FromExist P Φ → FromExist (<pers> P) (λ a, <pers> (Φ a))%I.
 Proof. rewrite /FromExist=> <-. by rewrite persistently_exist. Qed.
 Global Instance from_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
   FromExist P Φ → FromExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
@@ -625,7 +623,7 @@ Global Instance into_exist_pure {A} (φ : A → Prop) :
   @IntoExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /IntoExist pure_exist. Qed.
 Global Instance into_exist_affinely {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
+  IntoExist P Φ → IntoExist (<affine> P) (λ a, <affine> (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
 Global Instance into_exist_and_pure P Q φ :
   IntoPureT P φ → IntoExist (P ∧ Q) (λ _ : φ, Q).
@@ -641,10 +639,10 @@ Proof.
   rewrite -exist_intro //. apply sep_elim_r, _.
 Qed.
 Global Instance into_exist_absorbingly {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (bi_absorbingly P) (λ a, bi_absorbingly (Φ a))%I.
+  IntoExist P Φ → IntoExist (<absorb> P) (λ a, <absorb> (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP absorbingly_exist. Qed.
 Global Instance into_exist_persistently {A} P (Φ : A → PROP) :
-  IntoExist P Φ → IntoExist (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
+  IntoExist P Φ → IntoExist (<pers> P) (λ a, <pers> (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP persistently_exist. Qed.
 Global Instance into_exist_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
   IntoExist P Φ → IntoExist ⎡P⎤ (λ a, ⎡Φ a⎤%I).
@@ -654,10 +652,10 @@ Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
 Proof. by rewrite /IntoForall. Qed.
 Global Instance into_forall_affinely {A} P (Φ : A → PROP) :
-  IntoForall P Φ → IntoForall (bi_affinely P) (λ a, bi_affinely (Φ a))%I.
+  IntoForall P Φ → IntoForall (<affine> P) (λ a, <affine> (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
 Global Instance into_forall_persistently {A} P (Φ : A → PROP) :
-  IntoForall P Φ → IntoForall (bi_persistently P) (λ a, bi_persistently (Φ a))%I.
+  IntoForall P Φ → IntoForall (<pers> P) (λ a, <pers> (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP persistently_forall. Qed.
 Global Instance into_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall ⎡P⎤ (λ a, ⎡Φ a⎤%I).
@@ -689,12 +687,12 @@ Proof.
 Qed.
 
 Global Instance from_forall_affinely `{BiAffine PROP} {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall (bi_affinely P)%I (λ a, bi_affinely (Φ a))%I.
+  FromForall P Φ → FromForall (<affine> P) (λ a, <affine> (Φ a))%I.
 Proof.
   rewrite /FromForall=> <-. rewrite affine_affinely. by setoid_rewrite affinely_elim.
 Qed.
 Global Instance from_forall_persistently {A} P (Φ : A → PROP) :
-  FromForall P Φ → FromForall (bi_persistently P)%I (λ a, bi_persistently (Φ a))%I.
+  FromForall P Φ → FromForall (<pers> P)%I (λ a, <pers> (Φ a))%I.
 Proof. rewrite /FromForall=> <-. by rewrite persistently_forall. Qed.
 Global Instance from_forall_embed `{BiEmbed PROP PROP'} {A} P (Φ : A → PROP) :
   FromForall P Φ → FromForall ⎡P⎤%I (λ a, ⎡Φ a⎤%I).
@@ -717,7 +715,7 @@ Proof.
   rewrite /ElimModal=> H ?. apply forall_intro=> a. rewrite (forall_elim a); auto.
 Qed.
 Global Instance elim_modal_absorbingly_here P Q :
-  Absorbing Q → ElimModal True (bi_absorbingly P) P Q Q.
+  Absorbing Q → ElimModal True (<absorb> P) P Q Q.
 Proof.
   rewrite /ElimModal=> H.
   by rewrite absorbingly_sep_l wand_elim_r absorbing_absorbingly.
@@ -761,12 +759,12 @@ Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.
 Global Instance frame_here p R : Frame p R R emp | 1.
 Proof. intros. by rewrite /Frame affinely_persistently_if_elim sep_elim_l. Qed.
 Global Instance frame_affinely_here_absorbing p R :
-  Absorbing R → Frame p (bi_affinely R) R True | 0.
+  Absorbing R → Frame p (<affine> R) R True | 0.
 Proof.
   intros. rewrite /Frame affinely_persistently_if_elim affinely_elim.
   apply sep_elim_l, _.
 Qed.
-Global Instance frame_affinely_here p R : Frame p (bi_affinely R) R emp | 1.
+Global Instance frame_affinely_here p R : Frame p (<affine> R) R emp | 1.
 Proof.
   intros. rewrite /Frame affinely_persistently_if_elim affinely_elim.
   apply sep_elim_l, _.
@@ -804,11 +802,11 @@ Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
 Proof. apply right_id, _. Qed.
 Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P.
 Proof. intros. apply True_sep, _. Qed.
-Global Instance make_and_emp_l_absorbingly P : KnownLMakeSep True P (bi_absorbingly P) | 10.
+Global Instance make_and_emp_l_absorbingly P : KnownLMakeSep True P (<absorb> P) | 10.
 Proof. intros. by rewrite /KnownLMakeSep /MakeSep. Qed.
 Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
 Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
-Global Instance make_and_emp_r_absorbingly P : KnownRMakeSep P True (bi_absorbingly P) | 10.
+Global Instance make_and_emp_r_absorbingly P : KnownRMakeSep P True (<absorb> P) | 10.
 Proof. intros. by rewrite /KnownRMakeSep /MakeSep comm. Qed.
 Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
 Proof. by rewrite /MakeSep. Qed.
@@ -847,11 +845,11 @@ Global Instance make_and_true_r P : KnownRMakeAnd P True P.
 Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
 Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P.
 Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed.
-Global Instance make_and_emp_l_affinely P : KnownLMakeAnd emp P (bi_affinely P) | 10.
+Global Instance make_and_emp_l_affinely P : KnownLMakeAnd emp P (<affine> P) | 10.
 Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd. Qed.
 Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P.
 Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
-Global Instance make_and_emp_r_affinely P : KnownRMakeAnd P emp (bi_affinely P) | 10.
+Global Instance make_and_emp_r_affinely P : KnownRMakeAnd P emp (<affine> P) | 10.
 Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd comm. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. by rewrite /MakeAnd. Qed.
@@ -917,11 +915,11 @@ Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
 Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_emp. Qed.
 Global Instance make_affinely_affine P : Affine P → KnownMakeAffinely P P | 1.
 Proof. intros. by rewrite /KnownMakeAffinely /MakeAffinely affine_affinely. Qed.
-Global Instance make_affinely_default P : MakeAffinely P (bi_affinely P) | 100.
+Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
 Proof. by rewrite /MakeAffinely. Qed.
 
 Global Instance frame_affinely R P Q Q' :
-  Frame true R P Q → MakeAffinely Q Q' → Frame true R (bi_affinely P) Q'.
+  Frame true R P Q → MakeAffinely Q Q' → Frame true R (<affine> P) Q'.
 Proof.
   rewrite /Frame /MakeAffinely=> <- <- /=.
   by rewrite -{1}affinely_idemp affinely_sep_2.
@@ -935,11 +933,11 @@ Qed.
 (* Note: there is no point in having an instance `Absorbing P → MakeAbsorbingly P P`
 because framing will never turn a proposition that is not absorbing into
 something that is absorbing. *)
-Global Instance make_absorbingly_default P : MakeAbsorbingly P (bi_absorbingly P) | 100.
+Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
 Proof. by rewrite /MakeAbsorbingly. Qed.
 
 Global Instance frame_absorbingly p R P Q Q' :
-  Frame p R P Q → MakeAbsorbingly Q Q' → Frame p R (bi_absorbingly P) Q'.
+  Frame p R P Q → MakeAbsorbingly Q Q' → Frame p R (<absorb> P) Q'.
 Proof.
   rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
 Qed.
@@ -952,11 +950,11 @@ Proof.
      -persistently_True_emp persistently_pure.
 Qed.
 Global Instance make_persistently_default P :
-  MakePersistently P (bi_persistently P) | 100.
+  MakePersistently P (<pers> P) | 100.
 Proof. by rewrite /MakePersistently. Qed.
 
 Global Instance frame_persistently R P Q Q' :
-  Frame true R P Q → MakePersistently Q Q' → Frame true R (bi_persistently P) Q'.
+  Frame true R P Q → MakePersistently Q Q' → Frame true R (<pers> P) Q'.
 Proof.
   rewrite /Frame /MakePersistently=> <- <- /=.
   rewrite -persistently_and_affinely_sep_l.
@@ -1238,12 +1236,12 @@ Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
 (* FIXME: This instance is overly specific, generalize it. *)
 Global Instance into_sep_affinely_later `{!Timeless (emp%I : PROP)} P Q1 Q2 :
   IntoSep P Q1 Q2 → Affine Q1 → Affine Q2 →
-  IntoSep (bi_affinely (â–· P)) (bi_affinely (â–· Q1)) (bi_affinely (â–· Q2)).
+  IntoSep (<affine> â–· P) (<affine> â–· Q1) (<affine> â–· Q2).
 Proof.
   rewrite /IntoSep /= => -> ??.
   rewrite -{1}(affine_affinely Q1) -{1}(affine_affinely Q2) later_sep !later_affinely_1.
   rewrite -except_0_sep /sbi_except_0 affinely_or. apply or_elim, affinely_elim.
-  rewrite -(idemp bi_and (bi_affinely (â–· False))%I) persistent_and_sep_1.
+  rewrite -(idemp bi_and (<affine> â–· False)%I) persistent_and_sep_1.
   by rewrite -(False_elim Q1) -(False_elim Q2).
 Qed.
 
@@ -1438,16 +1436,16 @@ Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
   @IntoInternalEq PROP A (x ≡ y) x y.
 Proof. by rewrite /IntoInternalEq. Qed.
 Global Instance into_internal_eq_affinely {A : ofeT} (x y : A) P :
-  IntoInternalEq P x y → IntoInternalEq (bi_affinely P) x y.
+  IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
 Global Instance into_internal_eq_absorbingly {A : ofeT} (x y : A) P :
-  IntoInternalEq P x y → IntoInternalEq (bi_absorbingly P) x y.
+  IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
 Global Instance into_internal_eq_plainly `{BiPlainly PROP} {A : ofeT} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (■ P) x y.
 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.
+  IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
 Global Instance into_internal_eq_embed
        `{SbiEmbed PROP PROP'} {A : ofeT} (x y : A) P :
@@ -1463,16 +1461,16 @@ Global Instance into_except_0_later_if p P : Timeless P → IntoExcept0 (▷?p P
 Proof. rewrite /IntoExcept0. destruct p; auto using except_0_intro. Qed.
 
 Global Instance into_except_0_affinely P Q :
-  IntoExcept0 P Q → IntoExcept0 (bi_affinely P) (bi_affinely Q).
+  IntoExcept0 P Q → IntoExcept0 (<affine> P) (<affine> Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_affinely_2. Qed.
 Global Instance into_except_0_absorbingly P Q :
-  IntoExcept0 P Q → IntoExcept0 (bi_absorbingly P) (bi_absorbingly Q).
+  IntoExcept0 P Q → IntoExcept0 (<absorb> P) (<absorb> Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_absorbingly. Qed.
 Global Instance into_except_0_plainly `{BiPlainly PROP, BiPlainlyExist PROP} P Q :
   IntoExcept0 P Q → IntoExcept0 (■ P) (■ Q).
 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).
+  IntoExcept0 P Q → IntoExcept0 (<pers> P) (<pers> Q).
 Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
 Global Instance into_except_0_embed `{SbiEmbed PROP PROP'} P Q :
   IntoExcept0 P Q → IntoExcept0 ⎡P⎤ ⎡Q⎤.
@@ -1657,16 +1655,16 @@ Proof.
 Qed.
 
 Global Instance into_later_affinely n P Q :
-  IntoLaterN false n P Q → IntoLaterN false n (bi_affinely P) (bi_affinely Q).
+  IntoLaterN false n P Q → IntoLaterN false n (<affine> P) (<affine> Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_affinely_2. Qed.
 Global Instance into_later_absorbingly n P Q :
-  IntoLaterN false n P Q → IntoLaterN false n (bi_absorbingly P) (bi_absorbingly Q).
+  IntoLaterN false n P Q → IntoLaterN false n (<absorb> P) (<absorb> Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
 Global Instance into_later_plainly `{BiPlainly PROP} n P Q :
   IntoLaterN false n P Q → IntoLaterN false n (■ P) (■ Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_plainly. Qed.
 Global Instance into_later_persistently n P Q :
-  IntoLaterN false n P Q → IntoLaterN false n (bi_persistently P) (bi_persistently Q).
+  IntoLaterN false n P Q → IntoLaterN false n (<pers> P) (<pers> Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_persistently. Qed.
 Global Instance into_later_embed`{SbiEmbed PROP PROP'} n P Q :
   IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index b758e8b85bd351d555d5484e4bc46029ad238afc..158f06b0665fc15f981f87e3c330341aea180fcf 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -69,7 +69,7 @@ Hint Extern 0 (IntoPureT _ _) =>
     [IntoPure], we can have the same behavior by asking that [P] be
     [Affine]. *)
 Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
-  from_pure : bi_affinely_if a ⌜φ⌝ ⊢ P.
+  from_pure : <affine>?a ⌜φ⌝ ⊢ P.
 Arguments FromPure {_} _ _%I _%type_scope : simpl never.
 Arguments from_pure {_} _ _%I _%type_scope {_}.
 Hint Mode FromPure + + ! - : typeclass_instances.
@@ -89,7 +89,7 @@ Arguments into_internal_eq {_ _} _%I _%type_scope _%type_scope {_}.
 Hint Mode IntoInternalEq + - ! - - : typeclass_instances.
 
 Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
-  into_persistent : bi_persistently_if p P ⊢ bi_persistently Q.
+  into_persistent : <pers>?p P ⊢ <pers> Q.
 Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
@@ -108,7 +108,7 @@ introduce, [sel] should be an evar.
 For modalities [N] that do not need to augment the proof mode environment, one
 can define an instance [FromModal modality_id (N P) P]. Defining such an
 instance only imposes the proof obligation [P ⊢ N P]. Examples of such
-modalities [N] are [bupd], [fupd], [except_0], [monPred_relatively] and
+modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
 [bi_absorbingly]. *)
 Class FromModal {PROP1 PROP2 : bi} {A}
     (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
@@ -118,14 +118,14 @@ Arguments from_modal {_ _ _} _ _ _%I _%I {_}.
 Hint Mode FromModal - + - - - ! - : typeclass_instances.
 
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
-  from_affinely : bi_affinely Q ⊢ P.
+  from_affinely : <affine> Q ⊢ P.
 Arguments FromAffinely {_} _%I _%type_scope : simpl never.
 Arguments from_affinely {_} _%I _%type_scope {_}.
 Hint Mode FromAffinely + ! - : typeclass_instances.
 Hint Mode FromAffinely + - ! : typeclass_instances.
 
 Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
-  into_absorbingly : P ⊢ bi_absorbingly Q.
+  into_absorbingly : P ⊢ <absorb> Q.
 Arguments IntoAbsorbingly {_} _%I _%I.
 Arguments into_absorbingly {_} _%I _%I {_}.
 Hint Mode IntoAbsorbingly + ! -  : typeclass_instances.
@@ -340,7 +340,7 @@ Arguments KnownRMakeOr {_} _%I _%I _%I.
 Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
 
 Class MakeAffinely {PROP : bi} (P Q : PROP) :=
-  make_affinely : bi_affinely P ⊣⊢ Q.
+  make_affinely : <affine> P ⊣⊢ Q.
 Arguments MakeAffinely {_} _%I _%I.
 Hint Mode MakeAffinely + - - : typeclass_instances.
 Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
@@ -349,7 +349,7 @@ Arguments KnownMakeAffinely {_} _%I _%I.
 Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
 
 Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
-  make_absorbingly : bi_absorbingly P ⊣⊢ Q.
+  make_absorbingly : <absorb> P ⊣⊢ Q.
 Arguments MakeAbsorbingly {_} _%I _%I.
 Hint Mode MakeAbsorbingly + - - : typeclass_instances.
 Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
@@ -358,7 +358,7 @@ Arguments KnownMakeAbsorbingly {_} _%I _%I.
 Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
 
 Class MakePersistently {PROP : bi} (P Q : PROP) :=
-  make_persistently : bi_persistently P ⊣⊢ Q.
+  make_persistently : <pers> P ⊣⊢ Q.
 Arguments MakePersistently {_} _%I _%I.
 Hint Mode MakePersistently + - - : typeclass_instances.
 Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 91725a592729aeb9a17d01ac87b829c57643885f..4317e9e22fe8ff52956f2de46b6e67cf8ec85ade 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -418,7 +418,7 @@ Proof.
   rewrite {2}envs_clear_spatial_sound.
   rewrite (env_spatial_is_nil_affinely_persistently (envs_clear_spatial _)) //.
   rewrite -persistently_and_affinely_sep_l.
-  rewrite (and_elim_l (bi_persistently _)%I)
+  rewrite (and_elim_l (<pers> _)%I)
           persistently_and_affinely_sep_r affinely_persistently_elim.
   destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
   apply envs_split_go_sound in HΔ as ->; last first.
@@ -609,10 +609,10 @@ Proof.
   destruct p; simpl.
   - by rewrite -(into_persistent _ P) /= wand_elim_r.
   - destruct HPQ.
-    + rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
+    + rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
               (into_persistent _ P) wand_elim_r //.
-    + rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent _ P).
-      by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
+    + rewrite (_ : P = <pers>?false P)%I // (into_persistent _ P).
+      by rewrite {1}(persistent_absorbingly_affinely (<pers> _)%I)
                  absorbingly_sep_l wand_elim_r HQ.
 Qed.
 
@@ -640,7 +640,7 @@ Lemma tac_impl_intro_persistent Δ Δ' i P P' Q R :
 Proof.
   rewrite /FromImpl envs_entails_eq => <- ?? <-.
   rewrite envs_app_singleton_sound //=. apply impl_intro_l.
-  rewrite (_ : P = bi_persistently_if false P)%I // (into_persistent false P).
+  rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
   by rewrite persistently_and_affinely_sep_l wand_elim_r.
 Qed.
 Lemma tac_impl_intro_drop Δ P Q R :
@@ -666,10 +666,10 @@ Lemma tac_wand_intro_persistent Δ Δ' i P P' Q R :
 Proof.
   rewrite /FromWand envs_entails_eq => <- ? HPQ ? HQ.
   rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
-  - rewrite -(affine_affinely P) (_ : P = bi_persistently_if false P)%I //
+  - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
             (into_persistent _ P) wand_elim_r //.
   - rewrite (_ : P = â–¡?false P)%I // (into_persistent _ P).
-    by rewrite {1}(persistent_absorbingly_affinely (bi_persistently _)%I)
+    by rewrite {1}(persistent_absorbingly_affinely (<pers> _)%I)
                absorbingly_sep_l wand_elim_r HQ.
 Qed.
 Lemma tac_wand_intro_pure Δ P φ Q R :
@@ -791,7 +791,7 @@ Qed.
 
 Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
   envs_lookup j Δ = Some (q,P) →
-  envs_entails Δ (bi_absorbingly R) →
+  envs_entails Δ (<absorb> R) →
   IntoPersistent false R R' →
   (if q then TCTrue else BiAffine PROP) →
   envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' →
@@ -799,9 +799,9 @@ Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
 Proof.
   rewrite envs_entails_eq => ? HR ? Hpos ? <-. rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
   rewrite envs_replace_singleton_sound //; destruct q; simpl.
-  - by rewrite (_ : R = bi_persistently_if false R)%I // (into_persistent _ R)
+  - by rewrite (_ : R = <pers>?false R)%I // (into_persistent _ R)
       absorbingly_persistently sep_elim_r persistently_and_affinely_sep_l wand_elim_r.
-  - by rewrite (absorbing_absorbingly R) (_ : R = bi_persistently_if false R)%I //
+  - by rewrite (absorbing_absorbingly R) (_ : R = <pers>?false R)%I //
        (into_persistent _ R) sep_elim_r persistently_and_affinely_sep_l wand_elim_r.
 Qed.
 
@@ -809,7 +809,7 @@ Qed.
 [FromAssumption] magic. *)
 Lemma tac_specialize_persistent_helper_done Δ i q P :
   envs_lookup i Δ = Some (q,P) →
-  envs_entails Δ (bi_absorbingly P).
+  envs_entails Δ (<absorb> P).
 Proof.
   rewrite envs_entails_eq /bi_absorbingly=> /envs_lookup_sound=> ->.
   rewrite affinely_persistently_if_elim comm. f_equiv; auto.
@@ -838,7 +838,7 @@ Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
 Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
   IntoIH φ Δ P →
   env_spatial_is_nil Δ = true →
-  envs_entails Δ (bi_persistently P → Q) →
+  envs_entails Δ (<pers> P → Q) →
   envs_entails Δ Q.
 Proof.
   rewrite /IntoIH envs_entails_eq. intros HP ? HPQ.
@@ -1389,7 +1389,7 @@ Proof.
   rewrite envs_entails_eq => ?? HQ.
   rewrite (env_spatial_is_nil_affinely_persistently Δ) //.
   rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
-  rewrite -(löb (bi_persistently Q)%I) later_persistently. apply impl_intro_l.
+  rewrite -(löb (<pers> Q)%I) later_persistently. apply impl_intro_l.
   rewrite envs_app_singleton_sound //; simpl; rewrite HQ.
   rewrite persistently_and_affinely_sep_l -{1}affinely_persistently_idemp.
   by rewrite affinely_persistently_sep_2 wand_elim_r affinely_elim.
diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v
index 2ec838ca783a20824c23a26f13832360085a5179..814d93b996e626a265de741fed410e8d67c7e6df 100644
--- a/theories/proofmode/modalities.v
+++ b/theories/proofmode/modalities.v
@@ -154,7 +154,7 @@ End modality1.
 [P ⊢ M P]. This is done by defining an instance [FromModal modality_id (M P) P],
 which will instruct [iModIntro] to introduce the modality without modifying the
 proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
-[monPred_relatively] and [bi_absorbingly]. *)
+[monPred_subjectively] and [bi_absorbingly]. *)
 Lemma modality_id_mixin {PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
 Proof. split; simpl; eauto. Qed.
 Definition modality_id {PROP : bi} := Modality (@id PROP) modality_id_mixin.
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index fef4a9078ccfaa95a9ba85927ecc581908b42e1a..228e1d4549fa2610c6d0cfeff009eb2e72d071c0 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -18,18 +18,18 @@ Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
 Section modalities.
   Context {I : biIndex} {PROP : bi}.
 
-  Lemma modality_absolutely_mixin :
-    modality_mixin (@monPred_absolutely I PROP)
-      (MIEnvFilter Absolute) (MIEnvFilter Absolute).
+  Lemma modality_objectively_mixin :
+    modality_mixin (@monPred_objectively I PROP)
+      (MIEnvFilter Objective) (MIEnvFilter Objective).
   Proof.
     split; simpl; split_and?; intros;
       try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
-      eauto using bi.equiv_entails_sym, absolute_absolutely,
-        monPred_absolutely_mono, monPred_absolutely_and,
-        monPred_absolutely_sep_2 with typeclass_instances.
+      eauto using bi.equiv_entails_sym, objective_objectively,
+        monPred_objectively_mono, monPred_objectively_and,
+        monPred_objectively_sep_2 with typeclass_instances.
   Qed.
-  Definition modality_absolutely :=
-    Modality _ modality_absolutely_mixin.
+  Definition modality_objectively :=
+    Modality _ modality_objectively_mixin.
 End modalities.
 
 Section bi.
@@ -42,12 +42,12 @@ Implicit Types 𝓟 𝓠 𝓡 : PROP.
 Implicit Types φ : Prop.
 Implicit Types i j : I.
 
-Global Instance from_modal_absolutely P :
-  FromModal modality_absolutely (∀ᵢ P) (∀ᵢ P) P | 1.
+Global Instance from_modal_objectively P :
+  FromModal modality_objectively (<obj> P) (<obj> P) P | 1.
 Proof. by rewrite /FromModal. Qed.
-Global Instance from_modal_relatively P :
-  FromModal modality_id (∃ᵢ P) (∃ᵢ P) P | 1.
-Proof. by rewrite /FromModal /= -monPred_relatively_intro. Qed.
+Global Instance from_modal_subjectively P :
+  FromModal modality_id (<subj> P) (<subj> P) P | 1.
+Proof. by rewrite /FromModal /= -monPred_subjectively_intro. Qed.
 
 Global Instance from_modal_affinely_monPred_at `(sel : A) P Q 𝓠 i :
   FromModal modality_affinely sel P Q → MakeMonPredAt i Q 𝓠 →
@@ -96,21 +96,21 @@ Global Instance make_monPred_at_exists {A} i (Φ : A → monPred) (Ψ : A → PR
   (∀ a, MakeMonPredAt i (Φ a) (Ψ a)) → MakeMonPredAt i (∃ a, Φ a) (∃ a, Ψ a).
 Proof. rewrite /MakeMonPredAt monPred_at_exist=>H. by setoid_rewrite <- H. Qed.
 Global Instance make_monPred_at_persistently i P 𝓟 :
-  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (bi_persistently P) (bi_persistently 𝓟).
+  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (<pers> P) (<pers> 𝓟).
 Proof. by rewrite /MakeMonPredAt monPred_at_persistently=><-. Qed.
 Global Instance make_monPred_at_affinely i P 𝓟 :
-  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (bi_affinely P) (bi_affinely 𝓟).
+  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (<affine> P) (<affine> 𝓟).
 Proof. by rewrite /MakeMonPredAt monPred_at_affinely=><-. Qed.
 Global Instance make_monPred_at_absorbingly i P 𝓟 :
-  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (bi_absorbingly P) (bi_absorbingly 𝓟).
+  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (<absorb> P) (<absorb> 𝓟).
 Proof. by rewrite /MakeMonPredAt monPred_at_absorbingly=><-. 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 𝓟).
+  MakeMonPredAt i (<pers>?p P) (<pers>?p 𝓟).
 Proof. destruct p; simpl; apply _. Qed.
 Global Instance make_monPred_at_affinely_if i P 𝓟 p :
   MakeMonPredAt i P 𝓟 →
-  MakeMonPredAt i (bi_affinely_if p P) (bi_affinely_if p 𝓟).
+  MakeMonPredAt i (<affine>?p P) (<affine>?p 𝓟).
 Proof. destruct p; simpl; apply _. Qed.
 Global Instance make_monPred_at_embed i 𝓟 : MakeMonPredAt i ⎡𝓟⎤ 𝓟.
 Proof. by rewrite /MakeMonPredAt monPred_at_embed. Qed.
@@ -135,17 +135,17 @@ Proof.
   apply  bi.affinely_persistently_if_elim.
 Qed.
 
-Global Instance from_assumption_make_monPred_absolutely P Q :
-  FromAssumption p P Q → KnownLFromAssumption p (∀ᵢ P) Q.
+Global Instance from_assumption_make_monPred_objectively P Q :
+  FromAssumption p P Q → KnownLFromAssumption p (<obj> P) Q.
 Proof.
   intros ?.
-  by rewrite /KnownLFromAssumption /FromAssumption monPred_absolutely_elim.
+  by rewrite /KnownLFromAssumption /FromAssumption monPred_objectively_elim.
 Qed.
-Global Instance from_assumption_make_monPred_relatively P Q :
-  FromAssumption p P Q → KnownRFromAssumption p P (∃ᵢ Q).
+Global Instance from_assumption_make_monPred_subjectively P Q :
+  FromAssumption p P Q → KnownRFromAssumption p P (<subj> Q).
 Proof.
   intros ?.
-  by rewrite /KnownRFromAssumption /FromAssumption -monPred_relatively_intro.
+  by rewrite /KnownRFromAssumption /FromAssumption -monPred_subjectively_intro.
 Qed.
 
 Global Instance as_valid_monPred_at φ P (Φ : I → PROP) :
@@ -298,26 +298,26 @@ Proof.
   by rewrite monPred_at_exist.
 Qed.
 
-Global Instance from_forall_monPred_at_absolutely P (Φ : I → PROP) i :
-  (∀ i, MakeMonPredAt i P (Φ i)) → FromForall ((∀ᵢ P) i)%I Φ.
+Global Instance from_forall_monPred_at_objectively P (Φ : I → PROP) i :
+  (∀ i, MakeMonPredAt i P (Φ i)) → FromForall ((<obj> P) i)%I Φ.
 Proof.
-  rewrite /FromForall /MakeMonPredAt monPred_at_absolutely=>H. by setoid_rewrite <- H.
+  rewrite /FromForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
 Qed.
-Global Instance into_forall_monPred_at_absolutely P (Φ : I → PROP) i :
-  (∀ i, MakeMonPredAt i P (Φ i)) → IntoForall ((∀ᵢ P) i) Φ.
+Global Instance into_forall_monPred_at_objectively P (Φ : I → PROP) i :
+  (∀ i, MakeMonPredAt i P (Φ i)) → IntoForall ((<obj> P) i) Φ.
 Proof.
-  rewrite /IntoForall /MakeMonPredAt monPred_at_absolutely=>H. by setoid_rewrite <- H.
+  rewrite /IntoForall /MakeMonPredAt monPred_at_objectively=>H. by setoid_rewrite <- H.
 Qed.
 
 Global Instance from_exist_monPred_at_ex P (Φ : I → PROP) i :
-  (∀ i, MakeMonPredAt i P (Φ i)) → FromExist ((∃ᵢ P) i) Φ.
+  (∀ i, MakeMonPredAt i P (Φ i)) → FromExist ((<subj> P) i) Φ.
 Proof.
-  rewrite /FromExist /MakeMonPredAt monPred_at_relatively=>H. by setoid_rewrite <- H.
+  rewrite /FromExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
 Qed.
 Global Instance into_exist_monPred_at_ex P (Φ : I → PROP) i :
-  (∀ i, MakeMonPredAt i P (Φ i)) → IntoExist ((∃ᵢ P) i) Φ.
+  (∀ i, MakeMonPredAt i P (Φ i)) → IntoExist ((<subj> P) i) Φ.
 Proof.
-  rewrite /IntoExist /MakeMonPredAt monPred_at_relatively=>H. by setoid_rewrite <- H.
+  rewrite /IntoExist /MakeMonPredAt monPred_at_subjectively=>H. by setoid_rewrite <- H.
 Qed.
 
 Global Instance from_forall_monPred_at {A} P (Φ : A → monPred) (Ψ : A → PROP) i :
@@ -352,11 +352,11 @@ Proof.
                          ?monPred_at_persistently monPred_at_embed.
 Qed.
 
-Global Instance into_embed_absolute P :
-  Absolute P → IntoEmbed P (∀ i, P i).
+Global Instance into_embed_objective P :
+  Objective P → IntoEmbed P (∀ i, P i).
 Proof.
   rewrite /IntoEmbed=> ?.
-  by rewrite {1}(absolute_absolutely P) monPred_absolutely_unfold.
+  by rewrite {1}(objective_objectively P) monPred_objectively_unfold.
 Qed.
 
 Global Instance elim_modal_at_bupd_goal `{BiBUpd PROP} φ 𝓟 𝓟' Q Q' i :
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 6dbaf950b36b44ab9454d41c8929971c87e8ffd9..db29a560903ce62a50623e6b8f9dbf2686008002 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1392,9 +1392,9 @@ Instance copy_destruct_impl {PROP : bi} (P Q : PROP) :
 Instance copy_destruct_wand {PROP : bi} (P Q : PROP) :
   CopyDestruct Q → CopyDestruct (P -∗ Q).
 Instance copy_destruct_affinely {PROP : bi} (P : PROP) :
-  CopyDestruct P → CopyDestruct (bi_affinely P).
+  CopyDestruct P → CopyDestruct (<affine> P).
 Instance copy_destruct_persistently {PROP : bi} (P : PROP) :
-  CopyDestruct P → CopyDestruct (bi_persistently P).
+  CopyDestruct P → CopyDestruct (<pers> P).
 
 Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
   let ident :=
@@ -1967,8 +1967,8 @@ Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit.
 Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit.
 Hint Extern 1 (envs_entails _ (â–· _)) => iNext.
 Hint Extern 1 (envs_entails _ (â–  _)) => iAlways.
-Hint Extern 1 (envs_entails _ (bi_persistently _)) => iAlways.
-Hint Extern 1 (envs_entails _ (bi_affinely _)) => iAlways.
+Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways.
+Hint Extern 1 (envs_entails _ (<affine> _)) => iAlways.
 Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _.
 Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro.
 Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 329ec130b5eb485918c3780c215d7bdacb9a0fda..c43c2f5c3a9006a75242c42593d419e7aeeaf1db 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -44,7 +44,7 @@ Lemma test_unfold_constants : bar.
 Proof. iIntros (P) "HP //". Qed.
 
 Lemma test_iRewrite {A : ofeT} (x y : A) P :
-  □ (∀ z, P -∗ bi_affinely (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
+  □ (∀ z, P -∗ <affine> (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
 Proof.
   iIntros "#H1 H2".
   iRewrite (bi.internal_eq_sym x x with "[# //]").
@@ -53,7 +53,7 @@ Proof.
 Qed.
 
 Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
-  P ∧ emp -∗ emp ∧ Q -∗ bi_affinely (P ∗ Q).
+  P ∧ emp -∗ emp ∧ Q -∗ <affine> (P ∗ Q).
 Proof. iIntros "[#? _] [_ #?]". auto. Qed.
 
 Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∧ Q)%I.
@@ -118,7 +118,7 @@ Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P.
 Proof. iIntros "H". iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅). done. Qed.
 
 Lemma test_iFrame_pure {A : ofeT} (φ : Prop) (y z : A) :
-  φ → bi_affinely ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP).
+  φ → <affine> ⌜y ≡ z⌝ -∗ (⌜ φ ⌝ ∧ ⌜ φ ⌝ ∧ y ≡ z : PROP).
 Proof. iIntros (Hv) "#Hxy". iFrame (Hv) "Hxy". Qed.
 
 Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
@@ -138,12 +138,12 @@ Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
 Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
 Proof.
   iIntros "HF".
-  iAssert (bi_affinely False)%I with "[> -]" as %[].
+  iAssert (<affine> False)%I with "[> -]" as %[].
   by iMod "HF".
 Qed.
 
 Lemma test_iMod_affinely_timeless P `{!Timeless P} :
-  bi_affinely (▷ P) -∗ ◇ bi_affinely P.
+  <affine> ▷ P -∗ ◇ <affine> P.
 Proof. iIntros "H". iMod "H". done. Qed.
 
 Lemma test_iAssumption_False P : False -∗ P.
@@ -188,13 +188,13 @@ Lemma test_iNext_quantifier {A} (Φ : A → A → PROP) :
 Proof. iIntros "H". iNext. done. Qed.
 
 Lemma test_iFrame_persistent (P Q : PROP) :
-  □ P -∗ Q -∗ bi_persistently (P ∗ P) ∗ (P ∗ Q ∨ Q).
+  □ P -∗ Q -∗ <pers> (P ∗ P) ∗ (P ∗ Q ∨ Q).
 Proof. iIntros "#HP". iFrame "HP". iIntros "$". Qed.
 
-Lemma test_iSplit_persistently P Q : □ P -∗ bi_persistently (P ∗ P).
+Lemma test_iSplit_persistently P Q : □ P -∗ <pers> (P ∗ P).
 Proof. iIntros "#?". by iSplit. Qed.
 
-Lemma test_iSpecialize_persistent P Q : □ P -∗ (bi_persistently P → Q) -∗ Q.
+Lemma test_iSpecialize_persistent P Q : □ P -∗ (<pers> P → Q) -∗ Q.
 Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
 
 Lemma test_iDestruct_persistent P (Φ : nat → PROP) `{!∀ x, Persistent (Φ x)}:
@@ -242,14 +242,13 @@ Lemma test_iIntros_let P :
   ∀ Q, let R := emp%I in P -∗ R -∗ Q -∗ P ∗ Q.
 Proof. iIntros (Q R) "$ _ $". Qed.
 
-Lemma test_foo P Q :
-  bi_affinely (▷ (Q ≡ P)) -∗ bi_affinely (▷ Q) -∗ bi_affinely (▷ P).
+Lemma test_foo P Q : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof.
   iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ".
 Qed.
 
 Lemma test_iIntros_modalities `(!Absorbing P) :
-  (bi_persistently (▷ ∀  x : nat, ⌜ x = 0 ⌝ → ⌜ x = 0 ⌝ -∗ False -∗ P -∗ P))%I.
+  (<pers> (▷ ∀  x : nat, ⌜ x = 0 ⌝ → ⌜ x = 0 ⌝ -∗ False -∗ P -∗ P))%I.
 Proof.
   iIntros (x ??).
   iIntros "* **". (* Test that fast intros do not work under modalities *)
@@ -260,12 +259,11 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
   x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
 Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
 
-Lemma test_iNext_affine P Q :
-  bi_affinely (▷ (Q ≡ P)) -∗ bi_affinely (▷ Q) -∗ bi_affinely (▷ P).
+Lemma test_iNext_affine P Q : <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof. iIntros "#HPQ HQ !#". iNext. by iRewrite "HPQ" in "HQ". Qed.
 
 Lemma test_iAlways P Q R :
-  □ P -∗ bi_persistently Q → R -∗ bi_persistently (bi_affinely (bi_affinely P)) ∗ □ Q.
+  □ P -∗ <pers> Q → R -∗ <pers> <affine> <affine> P ∗ □ Q.
 Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
 
 (* A bunch of test cases from #127 to establish that tactics behave the same on
@@ -337,14 +335,14 @@ Lemma test_iNext_fail P Q a b c d e f g h i j:
 Proof. iIntros "H". iNext. done. Qed.
 
 Lemma test_specialize_affine_pure (φ : Prop) P :
-  φ → (bi_affinely ⌜φ⌝ -∗ P) ⊢ P.
+  φ → (<affine> ⌜φ⌝ -∗ P) ⊢ P.
 Proof.
   iIntros (Hφ) "H". by iSpecialize ("H" with "[% //]").
 Qed.
 
 Lemma test_assert_affine_pure (φ : Prop) P :
-  φ → P ⊢ P ∗ bi_affinely ⌜φ⌝.
-Proof. iIntros (Hφ). iAssert (bi_affinely ⌜φ⌝) with "[%]" as "$"; auto. Qed.
+  φ → P ⊢ P ∗ <affine> ⌜φ⌝.
+Proof. iIntros (Hφ). iAssert (<affine> ⌜φ⌝)%I with "[%]" as "$"; auto. Qed.
 Lemma test_assert_pure (φ : Prop) P :
   φ → P ⊢ P ∗ ⌜φ⌝.
 Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto. Qed.
diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index b702dd7450c75c73088f78016d31c5f77b2b3677..606dd94a4599a0bc2c4c4b294294a916afeab0f8 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -60,7 +60,7 @@ Section iris_tests.
     by iApply inv_alloc.
   Qed.
 
-  Lemma test_iInv_0 N P: inv N (bi_persistently P) ={⊤}=∗ ▷ P.
+  Lemma test_iInv_0 N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
   Proof.
     iIntros "#H".
     iInv N as "#H2" "Hclose".
@@ -70,7 +70,7 @@ Section iris_tests.
 
   Lemma test_iInv_1 N E P:
     ↑N ⊆ E →
-    inv N (bi_persistently P) ={E}=∗ ▷ P.
+    inv N (<pers> P) ={E}=∗ ▷ P.
   Proof.
     iIntros (?) "#H".
     iInv N as "#H2" "Hclose".
@@ -79,7 +79,7 @@ Section iris_tests.
   Qed.
 
   Lemma test_iInv_2 γ p N P:
-    cinv N γ (bi_persistently P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
+    cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
   Proof.
     iIntros "(#?&?)".
     iInv N as "(#HP&Hown)" "Hclose".
@@ -88,7 +88,7 @@ Section iris_tests.
   Qed.
 
   Lemma test_iInv_3 γ p1 p2 N P:
-    cinv N γ (bi_persistently P) ∗ cinv_own γ p1 ∗ cinv_own γ p2
+    cinv N γ (<pers> P) ∗ cinv_own γ p1 ∗ cinv_own γ p2
       ={⊤}=∗ cinv_own γ p1 ∗ cinv_own γ p2  ∗ ▷ P.
   Proof.
     iIntros "(#?&Hown1&Hown2)".
@@ -99,7 +99,7 @@ Section iris_tests.
 
   Lemma test_iInv_4 t N E1 E2 P:
     ↑N ⊆ E2 →
-    na_inv t N (bi_persistently P) ∗ na_own t E1 ∗ na_own t E2
+    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
          ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
@@ -112,7 +112,7 @@ Section iris_tests.
   (* test named selection of which na_own to use *)
   Lemma test_iInv_5 t N E1 E2 P:
     ↑N ⊆ E2 →
-    na_inv t N (bi_persistently P) ∗ na_own t E1 ∗ na_own t E2
+    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
@@ -124,7 +124,7 @@ Section iris_tests.
 
   Lemma test_iInv_6 t N E1 E2 P:
     ↑N ⊆ E1 →
-    na_inv t N (bi_persistently P) ∗ na_own t E1 ∗ na_own t E2
+    na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
@@ -137,7 +137,7 @@ Section iris_tests.
   (* test robustness in presence of other invariants *)
   Lemma test_iInv_7 t N1 N2 N3 E1 E2 P:
     ↑N3 ⊆ E1 →
-    inv N1 P ∗ na_inv t N3 (bi_persistently P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
+    inv N1 P ∗ na_inv t N3 (<pers> P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&#?&#?&Hown1&Hown2)".
@@ -158,7 +158,7 @@ Section iris_tests.
   (* test selection by hypothesis name instead of namespace *)
   Lemma test_iInv_9 t N1 N2 N3 E1 E2 P:
     ↑N3 ⊆ E1 →
-    inv N1 P ∗ na_inv t N3 (bi_persistently P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
+    inv N1 P ∗ na_inv t N3 (<pers> P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
@@ -170,7 +170,7 @@ Section iris_tests.
   (* test selection by hypothesis name instead of namespace *)
   Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
     ↑N3 ⊆ E1 →
-    inv N1 P ∗ na_inv t N3 (bi_persistently P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
+    inv N1 P ∗ na_inv t N3 (<pers> P) ∗ inv N2 P  ∗ na_own t E1 ∗ na_own t E2
       ={⊤}=∗ na_own t E1 ∗ na_own t E2  ∗ ▷ P.
   Proof.
     iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
@@ -180,7 +180,7 @@ Section iris_tests.
   Qed.
 
   (* test selection by ident name *)
-  Lemma test_iInv_11 N P: inv N (bi_persistently P) ={⊤}=∗ ▷ P.
+  Lemma test_iInv_11 N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
   Proof.
     let H := iFresh in
     (iIntros H; iInv H as "#H2" "Hclose").
@@ -189,7 +189,7 @@ Section iris_tests.
   Qed.
 
   (* error messages *)
-  Lemma test_iInv_12 N P: inv N (bi_persistently P) ={⊤}=∗ True.
+  Lemma test_iInv_12 N P: inv N (<pers> P) ={⊤}=∗ True.
   Proof.
     iIntros "H".
     Fail iInv 34 as "#H2" "Hclose".
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 5ae50a06ebd978e0ce85aaeb0ebdf2650f0439ac..1d4bcc5f97a5c86b2f0c0553bbeb380d09eb5e4a 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -69,22 +69,22 @@ Section tests.
     iIntros "H HP". by iApply "H".
   Qed.
 
-  Lemma test_absolutely P Q : ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ ∀ᵢ (P ∗ Q).
+  Lemma test_objectively P Q : <obj> emp -∗ <obj> P -∗ <obj> Q -∗ <obj> (P ∗ Q).
   Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.
 
-  Lemma test_absolutely_absorbing P Q R `{!Absorbing P} :
-    ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
+  Lemma test_objectively_absorbing P Q R `{!Absorbing P} :
+    <obj> emp -∗ <obj> P -∗ <obj> Q -∗ R -∗ <obj> (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
 
-  Lemma test_absolutely_affine P Q R `{!Affine R} :
-    ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
+  Lemma test_objectively_affine P Q R `{!Affine R} :
+    <obj> emp -∗ <obj> P -∗ <obj> Q -∗ R -∗ <obj> (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
 
   Lemma test_iModIntro_embed P `{!Affine Q} 𝓟 𝓠 :
     □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ 𝓟 ∗ 𝓠 ⎤.
   Proof. iIntros "#H1 _ H2 H3". iAlways. iFrame. Qed.
 
-  Lemma test_iModIntro_embed_absolute P `{!Absolute Q} 𝓟 𝓠 :
+  Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
     □ P -∗ Q -∗ ⎡𝓟⎤ -∗ ⎡𝓠⎤ -∗ ⎡ ∀ i, 𝓟 ∗ 𝓠 ∗ Q i ⎤.
   Proof. iIntros "#H1 H2 H3 H4". iAlways. iFrame. Qed.