From 2ba2ba1e18a0627bf936abdced9ff297d9d9860b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 3 Mar 2018 17:25:05 +0100
Subject: [PATCH] Notations <absorb>, <affine> and <pers>.

---
 theories/base_logic/derived.v           |   3 +-
 theories/base_logic/upred.v             |  25 +-
 theories/bi/big_op.v                    |  14 +-
 theories/bi/derived_connectives.v       |  26 +-
 theories/bi/derived_laws.v              | 308 ++++++++++--------------
 theories/bi/embedding.v                 |  13 +-
 theories/bi/fixpoint.v                  |   6 +-
 theories/bi/interface.v                 |  46 ++--
 theories/bi/monpred.v                   |  28 +--
 theories/bi/plainly.v                   |  35 ++-
 theories/program_logic/total_adequacy.v |   2 +-
 theories/proofmode/class_instances.v    | 150 ++++++------
 theories/proofmode/classes.v            |  14 +-
 theories/proofmode/coq_tactics.v        |  26 +-
 theories/proofmode/monpred.v            |  10 +-
 theories/proofmode/tactics.v            |   8 +-
 theories/tests/proofmode.v              |  32 ++-
 theories/tests/proofmode_iris.v         |  24 +-
 18 files changed, 358 insertions(+), 412 deletions(-)

diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index c126c3933..2bbd331ba 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 4284299a8..deb0ec4bb 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 d7648e928..a51063fdc 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 b687a3d4c..a381402bf 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 474bf1bb7..e55ac337d 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 c34bc95fe..247c09ff7 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 Φ).
diff --git a/theories/bi/fixpoint.v b/theories/bi/fixpoint.v
index ec42bf323..43f506b7b 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 5fd4fa0e9..955c22d42 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 44728ee10..11b0f5f99 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -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.
@@ -555,7 +555,7 @@ 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.
@@ -563,15 +563,13 @@ Lemma monPred_at_objectively i P : (<obj> P) i ⊣⊢ ∀ j, P j.
 Proof. by unseal. Qed.
 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).
@@ -700,20 +698,16 @@ Proof.
   rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
   rewrite (objective_at Q i). by rewrite (objective_at P k).
 Qed.
-Global Instance persistently_objective P `{!Objective P} :
-  Objective (bi_persistently P).
+Global Instance persistently_objective P `{!Objective P} : Objective (<pers> P).
 Proof. intros i j. unseal. by rewrite objective_at. Qed.
 
-Global Instance affinely_objective P `{!Objective P} : Objective (bi_affinely P).
+Global Instance affinely_objective P `{!Objective P} : Objective (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
-Global Instance absorbingly_objective P `{!Objective P} :
-  Objective (bi_absorbingly P).
+Global Instance absorbingly_objective P `{!Objective P} : Objective (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
-Global Instance persistently_if_objective P p `{!Objective P} :
-  Objective (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_objective P p `{!Objective P} :
-  Objective (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 *)
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index a3c7d83fb..7f63cc8bf 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 2cd2a6f3e..84954fee1 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 776f6a2ba..5898b0ae4 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,29 +27,29 @@ 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 → FromAssumption true P (bi_persistently Q).
+  FromAssumption true P Q → FromAssumption true P (<pers> Q).
 Proof.
   rewrite /FromAssumption /= =><-.
   by rewrite -{1}affinely_persistently_idemp affinely_elim.
 Qed.
 Global Instance from_assumption_affinely_r P Q :
-  FromAssumption true P Q → FromAssumption true P (bi_affinely Q).
+  FromAssumption true P Q → FromAssumption true P (<affine> Q).
 Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_idemp. Qed.
 Global Instance from_assumption_absorbingly_r p P Q :
-  FromAssumption p P Q → FromAssumption p P (bi_absorbingly Q).
+  FromAssumption p P Q → FromAssumption p P (<absorb> Q).
 Proof. rewrite /FromAssumption /= =><-. apply absorbingly_intro. Qed.
 
 Global Instance from_assumption_affinely_persistently_l p P Q :
   FromAssumption true P Q → FromAssumption p (□ P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim. Qed.
 Global Instance from_assumption_persistently_l_true P Q :
-  FromAssumption true P Q → FromAssumption true (bi_persistently P) Q.
+  FromAssumption true P Q → FromAssumption true (<pers> P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite persistently_idemp. Qed.
 Global Instance from_assumption_persistently_l_false `{BiAffine PROP} P Q :
-  FromAssumption true P Q → FromAssumption false (bi_persistently P) Q.
+  FromAssumption true P Q → FromAssumption false (<pers> P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite affine_affinely. Qed.
 Global Instance from_assumption_affinely_l_true p P Q :
-  FromAssumption p P Q → FromAssumption p (bi_affinely P) Q.
+  FromAssumption p P Q → FromAssumption p (<affine> P) Q.
 Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_elim. Qed.
 
 Global Instance from_assumption_forall {A} p (Φ : A → PROP) Q x :
@@ -89,13 +89,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⎤ φ.
@@ -154,20 +153,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⎤ φ.
@@ -175,13 +173,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.
@@ -196,11 +194,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.
@@ -210,7 +208,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
@@ -305,10 +303,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⎤.
@@ -355,11 +353,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 :
@@ -388,14 +386,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 :
@@ -439,7 +437,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.
@@ -447,7 +445,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.
@@ -466,7 +464,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.
@@ -496,23 +494,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.
@@ -546,14 +544,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⎤.
@@ -565,14 +563,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⎤.
@@ -585,13 +583,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).
@@ -604,7 +602,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).
@@ -620,10 +618,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).
@@ -633,10 +631,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).
@@ -668,12 +666,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).
@@ -696,7 +694,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.
@@ -740,12 +738,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, _.
@@ -783,11 +781,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.
@@ -826,11 +824,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.
@@ -896,11 +894,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.
@@ -914,11 +912,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.
@@ -931,11 +929,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.
@@ -1217,12 +1215,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.
 
@@ -1417,16 +1415,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 :
@@ -1442,16 +1440,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⎤.
@@ -1636,16 +1634,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 35b4ead6c..4e71e6897 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -59,7 +59,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.
@@ -79,7 +79,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,14 +108,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.
@@ -330,7 +330,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) :=
@@ -339,7 +339,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) :=
@@ -348,7 +348,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 91725a592..4317e9e22 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/monpred.v b/theories/proofmode/monpred.v
index 00c244408..77ae8ae82 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -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.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 5f2651d62..7266427ce 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 329ec130b..c43c2f5c3 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 b702dd745..606dd94a4 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".
-- 
GitLab