diff --git a/algebra/double_negation.v b/algebra/double_negation.v
index c3bd21a3f283476df187e631a9ba6a566e5f919c..875045d2211c5bcae82050a2482b5e83c6919248 100644
--- a/algebra/double_negation.v
+++ b/algebra/double_negation.v
@@ -23,8 +23,8 @@ Notation "P =n=★ Q" := (P -★ |=n=> Q)%I
   (at level 99, Q at level 200, format "P  =n=★  Q") : uPred_scope.
 
 (* Our goal is to prove that:
-  (1) |=n=> has (nearly) all the properties of the |=r=> modality that are used in Iris
-  (2) If our meta-logic is classical, then |=n=> and |=r=> are equivalent
+  (1) |=n=> has (nearly) all the properties of the |==> modality that are used in Iris
+  (2) If our meta-logic is classical, then |=n=> and |==> are equivalent
 *)
 
 Section bupd_nnupd.
@@ -264,7 +264,7 @@ Qed.
    direction from bupd to nnupd is similar to the proof of
    nnupd_ownM_updateP *)
 
-Lemma bupd_nnupd P: (|=r=> P) ⊢ |=n=> P.
+Lemma bupd_nnupd P: (|==> P) ⊢ |=n=> P.
 Proof.
   split. rewrite /uPred_nnupd. repeat uPred.unseal. intros n x ? Hbupd a.
   red; rewrite //= => n' yf ??.
@@ -282,7 +282,7 @@ Qed.
 (* However, the other direction seems to need a classical axiom: *)
 Section classical.
 Context (not_all_not_ex: ∀ (P : M → Prop), ¬ (∀ n : M, ¬ P n) → ∃ n : M, P n).
-Lemma nnupd_bupd P:  (|=n=> P) ⊢ (|=r=> P).
+Lemma nnupd_bupd P:  (|=n=> P) ⊢ (|==> P).
 Proof.
   rewrite /uPred_nnupd.
   split. uPred.unseal; red; rewrite //=.
@@ -373,8 +373,8 @@ Qed.
 
 (* Open question:
 
-   Do the basic properties of the |=r=> modality (bupd_intro, bupd_mono, rvs_trans, rvs_frame_r,
-      bupd_ownM_updateP, and adequacy) uniquely characterize |=r=>?
+   Do the basic properties of the |==> modality (bupd_intro, bupd_mono, rvs_trans, rvs_frame_r,
+      bupd_ownM_updateP, and adequacy) uniquely characterize |==>?
 *)
 
 End bupd_nnupd.
diff --git a/algebra/upred.v b/algebra/upred.v
index 79dd89383ef93a54bedfa3f5bc427098822068dd..c4b6e5da4cc6e38f2520d71c47d6a5671536a976 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -310,12 +310,12 @@ Notation "â–· P" := (uPred_later P)
   (at level 20, right associativity) : uPred_scope.
 Infix "≡" := uPred_eq : uPred_scope.
 Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope.
-Notation "|=r=> Q" := (uPred_bupd Q)
-  (at level 99, Q at level 200, format "|=r=>  Q") : uPred_scope.
-Notation "P =r=> Q" := (P ⊢ |=r=> Q)
+Notation "|==> Q" := (uPred_bupd Q)
+  (at level 99, Q at level 200, format "|==>  Q") : uPred_scope.
+Notation "P ==★ Q" := (P ⊢ |==> Q)
   (at level 99, Q at level 200, only parsing) : C_scope.
-Notation "P =r=★ Q" := (P -★ |=r=> Q)%I
-  (at level 99, Q at level 200, format "P  =r=★  Q") : uPred_scope.
+Notation "P ==★ Q" := (P -★ |==> Q)%I
+  (at level 99, Q at level 200, format "P  ==★  Q") : uPred_scope.
 
 Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
 Instance: Params (@uPred_iff) 1.
@@ -1283,20 +1283,20 @@ Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Qed.
 
 (* Basic update modality *)
-Lemma bupd_intro P : P =r=> P.
+Lemma bupd_intro P : P ==★ P.
 Proof.
   unseal. split=> n x ? HP k yf ?; exists x; split; first done.
   apply uPred_closed with n; eauto using cmra_validN_op_l.
 Qed.
-Lemma bupd_mono P Q : (P ⊢ Q) → (|=r=> P) =r=> Q.
+Lemma bupd_mono P Q : (P ⊢ Q) → (|==> P) ==★ Q.
 Proof.
   unseal. intros HPQ; split=> n x ? HP k yf ??.
   destruct (HP k yf) as (x'&?&?); eauto.
   exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
 Qed.
-Lemma bupd_trans P : (|=r=> |=r=> P) =r=> P.
+Lemma bupd_trans P : (|==> |==> P) ==★ P.
 Proof. unseal; split; naive_solver. Qed.
-Lemma bupd_frame_r P R : (|=r=> P) ★ R =r=> P ★ R.
+Lemma bupd_frame_r P R : (|==> P) ★ R ==★ P ★ R.
 Proof.
   unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
   destruct (HP k (x2 â‹… yf)) as (x'&?&?); eauto.
@@ -1306,7 +1306,7 @@ Proof.
   apply uPred_closed with n; eauto 3 using cmra_validN_op_l, cmra_validN_op_r.
 Qed.
 Lemma bupd_ownM_updateP x (Φ : M → Prop) :
-  x ~~>: Φ → uPred_ownM x =r=> ∃ y, ■ Φ y ∧ uPred_ownM y.
+  x ~~>: Φ → uPred_ownM x ==★ ∃ y, ■ Φ y ∧ uPred_ownM y.
 Proof.
   unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
   destruct (Hup k (Some (x3 â‹… yf))) as (y&?&?); simpl in *.
@@ -1320,20 +1320,20 @@ Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M).
 Proof. intros P Q; apply bupd_mono. Qed.
 Global Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_bupd M).
 Proof. intros P Q; apply bupd_mono. Qed.
-Lemma bupd_frame_l R Q : (R ★ |=r=> Q) =r=> R ★ Q.
+Lemma bupd_frame_l R Q : (R ★ |==> Q) ==★ R ★ Q.
 Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
-Lemma bupd_wand_l P Q : (P -★ Q) ★ (|=r=> P) =r=> Q.
+Lemma bupd_wand_l P Q : (P -★ Q) ★ (|==> P) ==★ Q.
 Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
-Lemma bupd_wand_r P Q : (|=r=> P) ★ (P -★ Q) =r=> Q.
+Lemma bupd_wand_r P Q : (|==> P) ★ (P -★ Q) ==★ Q.
 Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
-Lemma bupd_sep P Q : (|=r=> P) ★ (|=r=> Q) =r=> P ★ Q.
+Lemma bupd_sep P Q : (|==> P) ★ (|==> Q) ==★ P ★ Q.
 Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
-Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |=r=> uPred_ownM y.
+Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
 Proof.
   intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
   by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
 Qed.
-Lemma except_last_bupd P : ◇ (|=r=> P) ⊢ (|=r=> ◇ P).
+Lemma except_last_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P).
 Proof.
   rewrite /uPred_except_last. apply or_elim; auto using bupd_mono.
   by rewrite -bupd_intro -or_intro_l.
@@ -1490,9 +1490,9 @@ Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ★ Q.
 Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
 
 (** Consistency and adequancy statements *)
-Lemma adequacy φ n : (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) (■ φ)) → φ.
+Lemma adequacy φ n : (True ⊢ Nat.iter n (λ P, |==> ▷ P) (■ φ)) → φ.
 Proof.
-  cut (∀ x, ✓{n} x → Nat.iter n (λ P, |=r=> ▷ P)%I (■ φ)%I n x → φ).
+  cut (∀ x, ✓{n} x → Nat.iter n (λ P, |==> ▷ P)%I (■ φ)%I n x → φ).
   { intros help H. eapply (help ∅); eauto using ucmra_unit_validN.
     eapply H; try unseal; eauto using ucmra_unit_validN. }
   unseal. induction n as [|n IH]=> x Hx Hupd; auto.
@@ -1500,7 +1500,7 @@ Proof.
   eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
 Qed.
 
-Corollary consistency_modal n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False).
+Corollary consistency_modal n : ¬ (True ⊢ Nat.iter n (λ P, |==> ▷ P) False).
 Proof. exact (adequacy False n). Qed.
 
 Corollary consistency : ¬ (True ⊢ False).
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index d38861902e4b560118645bd1f66f6769d732c2db..be6417d58d13304065c0a58be382eba6fa1d5ec9 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -162,7 +162,7 @@ Proof.
 Qed.
 
 Lemma recv_split E l P1 P2 :
-  nclose N ⊆ E → recv l (P1 ★ P2) ={E}=> recv l P1 ★ recv l P2.
+  nclose N ⊆ E → recv l (P1 ★ P2) ={E}=★ recv l P1 ★ recv l P2.
 Proof.
   rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
   iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index 93f70b4078af4a97b0a109e68a7989417723745f..720ae3390df5ef4e7beb72bd78db8bdb1c164765 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -23,7 +23,7 @@ Proof.
   - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); eauto.
   - iIntros (l P) "!# [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
   - iIntros (l P) "!# Hl". iApply wait_spec; iFrame "Hl"; eauto.
-  - intros; by apply recv_split.
+  - iIntros (l P Q) "!#". by iApply recv_split.
   - apply recv_weaken.
 Qed.
 End spec.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index af2c649d6544bb84144e346f4aeeb5e3ef825741..a140c5b5bd1581132440b982012b7474b2d53237 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -40,7 +40,7 @@ Notation wptp t := ([★ list] ef ∈ t, WP ef {{ _, True }})%I.
 
 Lemma wp_step e1 σ1 e2 σ2 efs Φ :
   prim_step e1 σ1 e2 σ2 efs →
-  world σ1 ★ WP e1 {{ Φ }} =r=> ▷ |=r=> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp efs).
+  world σ1 ★ WP e1 {{ Φ }} ==★ ▷ |==> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp efs).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]".
   { iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. }
@@ -54,7 +54,7 @@ Qed.
 Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
   step (e1 :: t1,σ1) (t2, σ2) →
   world σ1 ★ WP e1 {{ Φ }} ★ wptp t1
-  =r=> ∃ e2 t2', t2 = e2 :: t2' ★ ▷ |=r=> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp t2').
+  ==★ ∃ e2 t2', t2 = e2 :: t2' ★ ▷ |==> ◇ (world σ2 ★ WP e2 {{ Φ }} ★ wptp t2').
 Proof.
   iIntros (Hstep) "(HW & He & Ht)".
   destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
@@ -69,7 +69,7 @@ Qed.
 Lemma wptp_steps n e1 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
   world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢
-  Nat.iter (S n) (λ P, |=r=> ▷ P) (∃ e2 t2',
+  Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 t2',
     t2 = e2 :: t2' ★ world σ2 ★ WP e2 {{ Φ }} ★ wptp t2').
 Proof.
   revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=.
@@ -79,11 +79,11 @@ Proof.
   iUpdIntro; iNext; iUpd "H" as ">?". by iApply IH.
 Qed.
 
-Instance bupd_iter_mono n : Proper ((⊢) ==> (⊢)) (Nat.iter n (λ P, |=r=> ▷ P)%I).
+Instance bupd_iter_mono n : Proper ((⊢) ==> (⊢)) (Nat.iter n (λ P, |==> ▷ P)%I).
 Proof. intros P Q HP. induction n; simpl; do 2?f_equiv; auto. Qed.
 
 Lemma bupd_iter_frame_l n R Q :
-  R ★ Nat.iter n (λ P, |=r=> ▷ P) Q ⊢ Nat.iter n (λ P, |=r=> ▷ P) (R ★ Q).
+  R ★ Nat.iter n (λ P, |==> ▷ P) Q ⊢ Nat.iter n (λ P, |==> ▷ P) (R ★ Q).
 Proof.
   induction n as [|n IH]; simpl; [done|].
   by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
@@ -92,7 +92,7 @@ Qed.
 Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
   nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) →
   world σ1 ★ WP e1 {{ v, ■ φ v }} ★ wptp t1 ⊢
-  Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■ φ v2).
+  Nat.iter (S (S n)) (λ P, |==> ▷ P) (■ φ v2).
 Proof.
   intros. rewrite wptp_steps //.
   rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
@@ -102,7 +102,7 @@ Proof.
 Qed.
 
 Lemma wp_safe e σ Φ :
-  world σ ★ WP e {{ Φ }} =r=> ▷ ■ (is_Some (to_val e) ∨ reducible e σ).
+  world σ ★ WP e {{ Φ }} ==★ ▷ ■ (is_Some (to_val e) ∨ reducible e σ).
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]".
   { iDestruct "H" as (v) "[% _]"; eauto 10. }
@@ -113,7 +113,7 @@ Qed.
 Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 →
   world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢
-  Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■ (is_Some (to_val e2) ∨ reducible e2 σ2)).
+  Nat.iter (S (S n)) (λ P, |==> ▷ P) (■ (is_Some (to_val e2) ∨ reducible e2 σ2)).
 Proof.
   intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
   iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq.
@@ -123,9 +123,9 @@ Qed.
 
 Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 I φ Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  (I ={⊤,∅}=> ∃ σ', ownP σ' ∧ ■ φ σ') →
+  (I ={⊤,∅}=★ ∃ σ', ownP σ' ∧ ■ φ σ') →
   I ★ world σ1 ★ WP e1 {{ Φ }} ★ wptp t1 ⊢
-  Nat.iter (S (S n)) (λ P, |=r=> ▷ P) (■ φ σ2).
+  Nat.iter (S (S n)) (λ P, |==> ▷ P) (■ φ σ2).
 Proof.
   intros ? HI. rewrite wptp_steps //.
   rewrite (Nat_iter_S_r (S n)) bupd_iter_frame_l. apply bupd_iter_mono.
@@ -156,8 +156,8 @@ Proof.
 Qed.
 
 Theorem wp_invariance Σ `{irisPreG Λ Σ} e σ1 t2 σ2 I φ Φ :
-  (∀ `{irisG Λ Σ}, ownP σ1 ={⊤}=> I ★ WP e {{ Φ }}) →
-  (∀ `{irisG Λ Σ}, I ={⊤,∅}=> ∃ σ', ownP σ' ∧ ■ φ σ') →
+  (∀ `{irisG Λ Σ}, ownP σ1 ={⊤}=★ I ★ WP e {{ Φ }}) →
+  (∀ `{irisG Λ Σ}, I ={⊤,∅}=★ ∃ σ', ownP σ' ∧ ■ φ σ') →
   rtc step ([e], σ1) (t2, σ2) →
   φ σ2.
 Proof.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 689b320795fb807c7eb5e6edeb07f886f4bbf3e5..d089851c4cad67fded140553e72479534903ab24 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -91,7 +91,7 @@ Section auth.
   Proof. intros a1 a2. apply auth_own_mono. Qed.
 
   Lemma auth_alloc_strong N E t (G : gset gname) :
-    ✓ (f t) → ▷ φ t ={E}=> ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
+    ✓ (f t) → ▷ φ t ={E}=★ ∃ γ, ■ (γ ∉ G) ∧ auth_ctx γ N f φ ∧ auth_own γ (f t).
   Proof.
     iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
     iUpd (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
@@ -102,17 +102,17 @@ Section auth.
   Qed.
 
   Lemma auth_alloc N E t :
-    ✓ (f t) → ▷ φ t ={E}=> ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t).
+    ✓ (f t) → ▷ φ t ={E}=★ ∃ γ, auth_ctx γ N f φ ∧ auth_own γ (f t).
   Proof.
     iIntros (?) "Hφ".
     iUpd (auth_alloc_strong N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
   Qed.
 
-  Lemma auth_empty γ : True =r=> auth_own γ ∅.
+  Lemma auth_empty γ : True ==★ auth_own γ ∅.
   Proof. by rewrite /auth_own -own_empty. Qed.
 
   Lemma auth_acc E γ a :
-    ▷ auth_inv γ f φ ★ auth_own γ a ={E}=> ∃ t,
+    ▷ auth_inv γ f φ ★ auth_own γ a ={E}=★ ∃ t,
       ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b,
       ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E}=★ ▷ auth_inv γ f φ ★ auth_own γ b.
   Proof.
@@ -128,7 +128,7 @@ Section auth.
 
   Lemma auth_open E N γ a :
     nclose N ⊆ E →
-    auth_ctx γ N f φ ★ auth_own γ a ={E,E∖N}=> ∃ t,
+    auth_ctx γ N f φ ★ auth_own γ a ={E,E∖N}=★ ∃ t,
       ■ (a ≼ f t) ★ ▷ φ t ★ ∀ u b,
       ■ ((f t, a) ~l~> (f u, b)) ★ ▷ φ u ={E∖N,E}=★ auth_own γ b.
   Proof.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index eedb29709a470cc57587daaaf95b661d253c3c9c..bfb964e97390d98e0fc73826e991626b98336740 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -63,7 +63,7 @@ Qed.
 
 Lemma box_own_auth_update γ b1 b2 b3 :
   box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2)
-  =r=> box_own_auth γ (● Excl' b3) ★ box_own_auth γ (◯ Excl' b3).
+  ==★ box_own_auth γ (● Excl' b3) ★ box_own_auth γ (◯ Excl' b3).
 Proof.
   rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
   by apply auth_update, option_local_update, exclusive_local_update.
@@ -86,7 +86,7 @@ Proof.
 Qed.
 
 Lemma box_insert f P Q :
-  ▷ box N f P ={N}=> ∃ γ, f !! γ = None ★
+  ▷ box N f P ={N}=★ ∃ γ, f !! γ = None ★
     slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P).
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
@@ -106,7 +106,7 @@ Qed.
 
 Lemma box_delete f P Q γ :
   f !! γ = Some false →
-  slice N γ Q ★ ▷ box N f P ={N}=> ∃ P',
+  slice N γ Q ★ ▷ box N f P ={N}=★ ∃ P',
     ▷ ▷ (P ≡ (Q ★ P')) ★ ▷ box N (delete γ f) P'.
 Proof.
   iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
@@ -125,7 +125,7 @@ Qed.
 
 Lemma box_fill f γ P Q :
   f !! γ = Some false →
-  slice N γ Q ★ ▷ Q ★ ▷ box N f P ={N}=> ▷ box N (<[γ:=true]> f) P.
+  slice N γ Q ★ ▷ Q ★ ▷ box N f P ={N}=★ ▷ box N (<[γ:=true]> f) P.
 Proof.
   iIntros (?) "(#Hinv & HQ & H)"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iInv N as (b') "(>Hγ & #HγQ & _)" "Hclose".
@@ -143,7 +143,7 @@ Qed.
 
 Lemma box_empty f P Q γ :
   f !! γ = Some true →
-  slice N γ Q ★ ▷ box N f P ={N}=> ▷ Q ★ ▷ box N (<[γ:=false]> f) P.
+  slice N γ Q ★ ▷ box N f P ={N}=★ ▷ Q ★ ▷ box N (<[γ:=false]> f) P.
 Proof.
   iIntros (?) "[#Hinv H]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iInv N as (b) "(>Hγ & #HγQ & HQ)" "Hclose".
@@ -160,7 +160,7 @@ Proof.
     iFrame; eauto.
 Qed.
 
-Lemma box_fill_all f P Q : box N f P ★ ▷ P ={N}=> box N (const true <$> f) P.
+Lemma box_fill_all f P Q : box N f P ★ ▷ P ={N}=★ box N (const true <$> f) P.
 Proof.
   iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
   iExists Φ; iSplitR; first by rewrite big_sepM_fmap.
@@ -176,7 +176,7 @@ Qed.
 
 Lemma box_empty_all f P Q :
   map_Forall (λ _, (true =)) f →
-  box N f P ={N}=> ▷ P ★ box N (const false <$> f) P.
+  box N f P ={N}=★ ▷ P ★ box N (const false <$> f) P.
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★
diff --git a/program_logic/cancelable_invariants.v b/program_logic/cancelable_invariants.v
index 8e526d1ea28f823d43121838572024da25e0e256..22f68d06d87c912579b84624b10ec814b911bb9d 100644
--- a/program_logic/cancelable_invariants.v
+++ b/program_logic/cancelable_invariants.v
@@ -44,7 +44,7 @@ Section proofs.
   Lemma cinv_own_1_l γ q : cinv_own γ 1 ★ cinv_own γ q ⊢ False.
   Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed.
 
-  Lemma cinv_alloc E N P : ▷ P ={E}=> ∃ γ, cinv N γ P ★ cinv_own γ 1.
+  Lemma cinv_alloc E N P : ▷ P ={E}=★ ∃ γ, cinv N γ P ★ cinv_own γ 1.
   Proof.
     rewrite /cinv /cinv_own. iIntros "HP".
     iUpd (own_alloc 1%Qp) as (γ) "H1"; first done.
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 3090c81535b3f16f19f663c189396ba503e968c0..7b1d8a00b42c5183d6eb3bfec547b83fadf12958 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -13,13 +13,13 @@ Module savedprop. Section savedprop.
   Context (sprop : Type) (saved : sprop → iProp → iProp).
   Hypothesis sprop_persistent : ∀ i P, PersistentP (saved i P).
   Hypothesis sprop_alloc_dep :
-    ∀ (P : sprop → iProp), True =r=> (∃ i, saved i (P i)).
+    ∀ (P : sprop → iProp), True ==★ (∃ i, saved i (P i)).
   Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q).
 
   (** A bad recursive reference: "Assertion with name [i] does not hold" *)
   Definition A (i : sprop) : iProp := ∃ P, ¬ P ★ saved i P.
 
-  Lemma A_alloc : True =r=> ∃ i, saved i (A i).
+  Lemma A_alloc : True ==★ ∃ i, saved i (A i).
   Proof. by apply sprop_alloc_dep. Qed.
 
   Lemma saved_NA i : saved i (A i) ⊢ ¬ A i.
diff --git a/program_logic/fancy_updates.v b/program_logic/fancy_updates.v
index 874fcb5d430d33fd8d19f045f8563d0b6313c642..f1c5ec814bf1606aff0793d27a7bbe872a688151 100644
--- a/program_logic/fancy_updates.v
+++ b/program_logic/fancy_updates.v
@@ -6,7 +6,7 @@ Import uPred.
 
 Program Definition fupd_def `{irisG Λ Σ}
     (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
-  (wsat ★ ownE E1 =r=★ ◇ (wsat ★ ownE E2 ★ P))%I.
+  (wsat ★ ownE E1 ==★ ◇ (wsat ★ ownE E2 ★ P))%I.
 Definition fupd_aux : { x | x = @fupd_def }. by eexists. Qed.
 Definition fupd := proj1_sig fupd_aux.
 Definition fupd_eq : @fupd = @fupd_def := proj2_sig fupd_aux.
@@ -19,7 +19,7 @@ Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
 Notation "P ={ E1 , E2 }=★ Q" := (P -★ |={E1,E2}=> Q)%I
   (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=★  Q") : uPred_scope.
-Notation "P ={ E1 , E2 }=> Q" := (P ⊢ |={E1,E2}=> Q)
+Notation "P ={ E1 , E2 }=★ Q" := (P ⊢ |={E1,E2}=> Q)
   (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
 
 Notation "|={ E }=> Q" := (fupd E E Q)
@@ -28,7 +28,7 @@ Notation "|={ E }=> Q" := (fupd E E Q)
 Notation "P ={ E }=★ Q" := (P -★ |={E}=> Q)%I
   (at level 99, E at level 50, Q at level 200,
    format "P  ={ E }=★  Q") : uPred_scope.
-Notation "P ={ E }=> Q" := (P ⊢ |={E}=> Q)
+Notation "P ={ E }=★ Q" := (P ⊢ |={E}=> Q)
   (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
 
 Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I
@@ -55,31 +55,31 @@ Proof.
   by iFrame.
 Qed.
 
-Lemma except_last_fupd E1 E2 P : â—‡ (|={E1,E2}=> P) ={E1,E2}=> P.
+Lemma except_last_fupd E1 E2 P : ◇ (|={E1,E2}=> P) ={E1,E2}=★ P.
 Proof.
   rewrite fupd_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame.
 Qed.
 
-Lemma bupd_fupd E P : (|=r=> P) ={E}=> P.
+Lemma bupd_fupd E P : (|==> P) ={E}=★ P.
 Proof.
   rewrite fupd_eq /fupd_def. iIntros "H [$ $]"; iUpd "H".
   iUpdIntro. by iApply except_last_intro.
 Qed.
 
-Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=> Q.
+Lemma fupd_mono E1 E2 P Q : (P ⊢ Q) → (|={E1,E2}=> P) ={E1,E2}=★ Q.
 Proof.
   rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE".
   rewrite -HPQ. by iApply "HP".
 Qed.
 
-Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=> P.
+Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}=★ P.
 Proof.
   rewrite fupd_eq /fupd_def. iIntros "HP HwE".
   iUpd ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
 Qed.
 
 Lemma fupd_mask_frame_r' E1 E2 Ef P :
-  E1 ⊥ Ef → (|={E1,E2}=> E2 ⊥ Ef → P) ={E1 ∪ Ef,E2 ∪ Ef}=> P.
+  E1 ⊥ Ef → (|={E1,E2}=> E2 ⊥ Ef → P) ={E1 ∪ Ef,E2 ∪ Ef}=★ P.
 Proof.
   intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
   iUpd ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
@@ -87,7 +87,7 @@ Proof.
   iUpdIntro; iApply except_last_intro. by iApply "HP".
 Qed.
 
-Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=> P ★ Q.
+Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=★ P ★ Q.
 Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
 
 (** * Derived rules *)
@@ -97,50 +97,50 @@ Global Instance fupd_flip_mono' E1 E2 :
   Proper (flip (⊢) ==> flip (⊢)) (@fupd Λ Σ _ E1 E2).
 Proof. intros P Q; apply fupd_mono. Qed.
 
-Lemma fupd_intro E P : P ={E}=> P.
+Lemma fupd_intro E P : P ={E}=★ P.
 Proof. iIntros "HP". by iApply bupd_fupd. Qed.
 Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → True ⊢ |={E1,E2}=> |={E2,E1}=> True.
 Proof. exact: fupd_intro_mask. Qed.
-Lemma fupd_except_last E1 E2 P : (|={E1,E2}=> â—‡ P) ={E1,E2}=> P.
+Lemma fupd_except_last E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=★ P.
 Proof. by rewrite {1}(fupd_intro E2 P) except_last_fupd fupd_trans. Qed.
 
-Lemma fupd_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ={E1,E2}=> P ★ Q.
+Lemma fupd_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ={E1,E2}=★ P ★ Q.
 Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
-Lemma fupd_wand_l E1 E2 P Q : (P -★ Q) ★ (|={E1,E2}=> P) ={E1,E2}=> Q.
+Lemma fupd_wand_l E1 E2 P Q : (P -★ Q) ★ (|={E1,E2}=> P) ={E1,E2}=★ Q.
 Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
-Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=> Q.
+Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ★ (P -★ Q) ={E1,E2}=★ Q.
 Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
 
 Lemma fupd_trans_frame E1 E2 E3 P Q :
-  ((Q ={E2,E3}=★ True) ★ |={E1,E2}=> (Q ★ P)) ={E1,E3}=> P.
+  ((Q ={E2,E3}=★ True) ★ |={E1,E2}=> (Q ★ P)) ={E1,E3}=★ P.
 Proof.
   rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
   by rewrite fupd_frame_r left_id fupd_trans.
 Qed.
 
 Lemma fupd_mask_frame_r E1 E2 Ef P :
-  E1 ⊥ Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=> P.
+  E1 ⊥ Ef → (|={E1,E2}=> P) ={E1 ∪ Ef,E2 ∪ Ef}=★ P.
 Proof.
   iIntros (?) "H". iApply fupd_mask_frame_r'; auto.
   iApply fupd_wand_r; iFrame "H"; eauto.
 Qed.
-Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=> P.
+Lemma fupd_mask_mono E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ={E2}=★ P.
 Proof.
   intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
 Qed.
 
-Lemma fupd_sep E P Q : (|={E}=> P) ★ (|={E}=> Q) ={E}=> P ★ Q.
+Lemma fupd_sep E P Q : (|={E}=> P) ★ (|={E}=> Q) ={E}=★ P ★ Q.
 Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
 Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K → A → iProp Σ) (m : gmap K A) :
-  ([★ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=> [★ map] k↦x ∈ m, Φ k x.
+  ([★ map] k↦x ∈ m, |={E}=> Φ k x) ={E}=★ [★ map] k↦x ∈ m, Φ k x.
 Proof.
-  apply (big_opM_forall (λ P Q, P ={E}=> Q)); auto using fupd_intro.
+  apply (big_opM_forall (λ P Q, P ={E}=★ Q)); auto using fupd_intro.
   intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
 Qed.
 Lemma fupd_big_sepS `{Countable A} E (Φ : A → iProp Σ) X :
-  ([★ set] x ∈ X, |={E}=> Φ x) ={E}=> [★ set] x ∈ X, Φ x.
+  ([★ set] x ∈ X, |={E}=> Φ x) ={E}=★ [★ set] x ∈ X, Φ x.
 Proof.
-  apply (big_opS_forall (λ P Q, P ={E}=> Q)); auto using fupd_intro.
+  apply (big_opS_forall (λ P Q, P ={E}=★ Q)); auto using fupd_intro.
   intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
 Qed.
 End fupd.
@@ -154,7 +154,7 @@ Section proofmode_classes.
   Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.
 
   Global Instance from_assumption_fupd E p P Q :
-    FromAssumption p P (|=r=> Q) → FromAssumption p P (|={E}=> Q)%I.
+    FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I.
   Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
 
   Global Instance into_wand_fupd E1 E2 R P Q :
@@ -186,7 +186,7 @@ Section proofmode_classes.
   Proof. by rewrite /FromUpd -bupd_fupd. Qed.
 
   Global Instance elim_upd_bupd_fupd E1 E2 P Q :
-    ElimUpd (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
+    ElimUpd (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
   Proof. by rewrite /ElimUpd (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans. Qed.
   Global Instance elim_upd_fupd_fupd E1 E2 E3 P Q :
     ElimUpd (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 334465548739514ad839c34be5e4fe0e7a2f349e..826dd12349a0d5c1709f2f0f78073adc93b12c8b 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -86,7 +86,7 @@ Proof. rewrite !own_eq /own_def; apply _. Qed.
 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
 Lemma own_alloc_strong a (G : gset gname) :
-  ✓ a → True =r=> ∃ γ, ■ (γ ∉ G) ∧ own γ a.
+  ✓ a → True ==★ ∃ γ, ■ (γ ∉ G) ∧ own γ a.
 Proof.
   intros Ha.
   rewrite -(bupd_mono (∃ m, ■ (∃ γ, γ ∉ G ∧ m = iRes_singleton γ a) ∧ uPred_ownM m)%I).
@@ -97,14 +97,14 @@ Proof.
   - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
     by rewrite !own_eq /own_def -(exist_intro γ) pure_equiv // left_id.
 Qed.
-Lemma own_alloc a : ✓ a → True =r=> ∃ γ, own γ a.
+Lemma own_alloc a : ✓ a → True ==★ ∃ γ, own γ a.
 Proof.
   intros Ha. rewrite (own_alloc_strong a ∅) //; [].
   apply bupd_mono, exist_mono=>?. eauto with I.
 Qed.
 
 (** ** Frame preserving updates *)
-Lemma own_updateP P γ a : a ~~>: P → own γ a =r=> ∃ a', ■ P a' ∧ own γ a'.
+Lemma own_updateP P γ a : a ~~>: P → own γ a ==★ ∃ a', ■ P a' ∧ own γ a'.
 Proof.
   intros Ha. rewrite !own_eq.
   rewrite -(bupd_mono (∃ m, ■ (∃ a', m = iRes_singleton γ a' ∧ P a') ∧ uPred_ownM m)%I).
@@ -115,16 +115,16 @@ Proof.
     rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
 Qed.
 
-Lemma own_update γ a a' : a ~~> a' → own γ a =r=> own γ a'.
+Lemma own_update γ a a' : a ~~> a' → own γ a ==★ own γ a'.
 Proof.
   intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
   by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
 Qed.
 Lemma own_update_2 γ a1 a2 a' :
-  a1 ⋅ a2 ~~> a' → own γ a1 ★ own γ a2 =r=> own γ a'.
+  a1 ⋅ a2 ~~> a' → own γ a1 ★ own γ a2 ==★ own γ a'.
 Proof. intros. rewrite -own_op. by apply own_update. Qed.
 Lemma own_update_3 γ a1 a2 a3 a' :
-  a1 ⋅ a2 ⋅ a3 ~~> a' → own γ a1 ★ own γ a2 ★ own γ a3 =r=> own γ a'.
+  a1 ⋅ a2 ⋅ a3 ~~> a' → own γ a1 ★ own γ a2 ★ own γ a3 ==★ own γ a'.
 Proof. intros. rewrite -!own_op assoc. by apply own_update. Qed.
 End global.
 
@@ -138,7 +138,7 @@ Arguments own_update {_ _} [_] _ _ _ _.
 Arguments own_update_2 {_ _} [_] _ _ _ _ _.
 Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 
-Lemma own_empty `{inG Σ (A:ucmraT)} γ : True =r=> own γ ∅.
+Lemma own_empty `{inG Σ (A:ucmraT)} γ : True ==★ own γ ∅.
 Proof.
   rewrite ownM_empty !own_eq /own_def.
   apply bupd_ownM_update, iprod_singleton_update_empty.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 8749825a3db5df94779e622d2eb68f10f1829436..0a5bda89a793cb14c6ce7b7df439e2cae9ec29e7 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -29,7 +29,7 @@ Qed.
 Global Instance inv_persistent N P : PersistentP (inv N P).
 Proof. rewrite inv_eq /inv; apply _. Qed.
 
-Lemma inv_alloc N E P : â–· P ={E}=> inv N P.
+Lemma inv_alloc N E P : ▷ P ={E}=★ inv N P.
 Proof.
   rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
   iUpd (ownI_alloc (∈ nclose N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
@@ -43,7 +43,7 @@ Proof.
 Qed.
 
 Lemma inv_open E N P :
-  nclose N ⊆ E → inv N P ={E,E∖N}=> ▷ P ★ (▷ P ={E∖N,E}=★ True).
+  nclose N ⊆ E → inv N P ={E,E∖N}=★ ▷ P ★ (▷ P ={E∖N,E}=★ True).
 Proof.
   rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
   iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
@@ -55,7 +55,7 @@ Proof.
 Qed.
 
 Lemma inv_open_timeless E N P `{!TimelessP P} :
-  nclose N ⊆ E → inv N P ={E,E∖N}=> P ★ (P ={E∖N,E}=★ True).
+  nclose N ⊆ E → inv N P ={E,E∖N}=★ P ★ (P ={E∖N,E}=★ True).
 Proof.
   iIntros (?) "Hinv". iUpd (inv_open with "Hinv") as "[>HP Hclose]"; auto.
   iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 4c44996616bbc56580b3d8154b86805d3e1e9e3b..235c246e384a48d78608c3737429d094a8e2c607 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -26,10 +26,10 @@ Section saved_prop.
   Proof. rewrite /saved_prop_own; apply _. Qed.
 
   Lemma saved_prop_alloc_strong x (G : gset gname) :
-    True =r=> ∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ x.
+    True ==★ ∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ x.
   Proof. by apply own_alloc_strong. Qed.
 
-  Lemma saved_prop_alloc x : True =r=> ∃ γ, saved_prop_own γ x.
+  Lemma saved_prop_alloc x : True ==★ ∃ γ, saved_prop_own γ x.
   Proof. by apply own_alloc. Qed.
 
   Lemma saved_prop_agree γ x y :
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 8b8ac17014fc6b58532490f102b42b82e2892596..a6861685aca2252155617b78443988a10d5a1ebe 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -68,12 +68,12 @@ Section sts.
      sts_frag_included. *)
   Lemma sts_ownS_weaken γ S1 S2 T1 T2 :
     T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 →
-    sts_ownS γ S1 T1 =r=> sts_ownS γ S2 T2.
+    sts_ownS γ S1 T1 ==★ sts_ownS γ S2 T2.
   Proof. intros ???. by apply own_update, sts_update_frag. Qed.
 
   Lemma sts_own_weaken γ s S T1 T2 :
     T2 ⊆ T1 → s ∈ S → sts.closed S T2 →
-    sts_own γ s T1 =r=> sts_ownS γ S T2.
+    sts_own γ s T1 ==★ sts_ownS γ S T2.
   Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
 
   Lemma sts_ownS_op γ S1 S2 T1 T2 :
@@ -82,7 +82,7 @@ Section sts.
   Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
 
   Lemma sts_alloc E N s :
-    ▷ φ s ={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s).
+    ▷ φ s ={E}=★ ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s).
   Proof.
     iIntros "Hφ". rewrite /sts_ctx /sts_own.
     iUpd (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
@@ -93,7 +93,7 @@ Section sts.
   Qed.
 
   Lemma sts_accS E γ S T :
-    ▷ sts_inv γ φ ★ sts_ownS γ S T ={E}=> ∃ s,
+    ▷ sts_inv γ φ ★ sts_ownS γ S T ={E}=★ ∃ s,
       ■ (s ∈ S) ★ ▷ φ s ★ ∀ s' T',
       ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E}=★ ▷ sts_inv γ φ ★ sts_own γ s' T'.
   Proof.
@@ -111,14 +111,14 @@ Section sts.
   Qed.
 
   Lemma sts_acc E γ s0 T :
-    ▷ sts_inv γ φ ★ sts_own γ s0 T ={E}=> ∃ s,
+    ▷ sts_inv γ φ ★ sts_own γ s0 T ={E}=★ ∃ s,
       ■ sts.frame_steps T s0 s ★ ▷ φ s ★ ∀ s' T',
       ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E}=★ ▷ sts_inv γ φ ★ sts_own γ s' T'.
   Proof. by apply sts_accS. Qed.
     
   Lemma sts_openS E N γ S T :
     nclose N ⊆ E →
-    sts_ctx γ N φ ★ sts_ownS γ S T ={E,E∖N}=> ∃ s,
+    sts_ctx γ N φ ★ sts_ownS γ S T ={E,E∖N}=★ ∃ s,
       ■ (s ∈ S) ★ ▷ φ s ★ ∀ s' T',
       ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E∖N,E}=★ sts_own γ s' T'.
   Proof.
@@ -136,7 +136,7 @@ Section sts.
 
   Lemma sts_open E N γ s0 T :
     nclose N ⊆ E →
-    sts_ctx γ N φ ★ sts_own γ s0 T ={E,E∖N}=> ∃ s,
+    sts_ctx γ N φ ★ sts_own γ s0 T ={E,E∖N}=★ ∃ s,
       ■ (sts.frame_steps T s0 s) ★ ▷ φ s ★ ∀ s' T',
       ■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ={E∖N,E}=★ sts_own γ s' T'.
   Proof. by apply sts_openS. Qed.
diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v
index 0d7ccc35926d46cba98cefd059abdd29fcfacdc5..7f389847c6b54a70ad71a0663be52de1d489e901 100644
--- a/program_logic/thread_local.v
+++ b/program_logic/thread_local.v
@@ -37,7 +37,7 @@ Section proofs.
   Global Instance tl_inv_persistent tid N P : PersistentP (tl_inv tid N P).
   Proof. rewrite /tl_inv; apply _. Qed.
 
-  Lemma tl_alloc : True =r=> ∃ tid, tl_own tid ⊤.
+  Lemma tl_alloc : True ==★ ∃ tid, tl_own tid ⊤.
   Proof. by apply own_alloc. Qed.
 
   Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 ★ tl_own tid E2 ⊢ ■ (E1 ⊥ E2).
@@ -51,7 +51,7 @@ Section proofs.
     intros ?. by rewrite /tl_own -own_op pair_op left_id coPset_disj_union.
   Qed.
 
-  Lemma tl_inv_alloc tid E N P : â–· P ={E}=> tl_inv tid N P.
+  Lemma tl_inv_alloc tid E N P : ▷ P ={E}=★ tl_inv tid N P.
   Proof.
     iIntros "HP".
     iUpd (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 3688fc337f41cb22e32a591a0a34723cd1858391..defadd5c1b797331b57e6fdeb999c60d28795b6f 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -13,6 +13,13 @@ Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
   (at level 99, E at level 50, Q at level 200,
    format "P  ={ E }=>  Q") : uPred_scope.
 
+Notation "P ={ E1 , E2 }=> Q" := (True ⊢ P ={E1,E2}=> Q)%I
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }=>  Q") : C_scope.
+Notation "P ={ E }=> Q" := (True ⊢ P ={E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=>  Q") : C_scope.
+
 Notation "P ={ E1 , E2 }â–·=> Q" := (P ={E1,E2}=> â–· |={E2,E1}=> Q)%I
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "P ={ E1 , E2 }â–·=>  Q") : uPred_scope.
@@ -39,9 +46,9 @@ Global Instance vs_mono' E1 E2 : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (vs E1
 Proof. solve_proper. Qed.
 
 Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
-Proof. iIntros "[]". Qed.
+Proof. iIntros "!# []". Qed.
 Lemma vs_timeless E P : TimelessP P → ▷ P ={E}=> P.
-Proof. by iIntros (?) "> ?". Qed.
+Proof. by iIntros (?) "!# > ?". Qed.
 
 Lemma vs_transitive E1 E2 E3 P Q R :
   (P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R) ⊢ P ={E1,E3}=> R.
@@ -51,7 +58,7 @@ Proof.
 Qed.
 
 Lemma vs_reflexive E P : P ={E}=> P.
-Proof. by iIntros "HP". Qed.
+Proof. by iIntros "!# HP". Qed.
 
 Lemma vs_impl E P Q : □ (P → Q) ⊢ P ={E}=> Q.
 Proof. iIntros "#HPQ !# HP". by iApply "HPQ". Qed.
@@ -77,5 +84,5 @@ Proof.
 Qed.
 
 Lemma vs_alloc N P : â–· P ={N}=> inv N P.
-Proof. iIntros "HP". by iApply inv_alloc. Qed.
+Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
 End vs.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 9c0f14e089f05c613458f770126e39e812bf92ab..582174638a2b0f530473867e66b17315f0e3dded 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -82,7 +82,7 @@ Proof.
   iIntros "HΦ". rewrite wp_unfold /wp_pre.
   iLeft; iExists v; rewrite to_of_val; auto.
 Qed.
-Lemma wp_value_inv E Φ v : WP of_val v @ E {{ Φ }} ={E}=> Φ v.
+Lemma wp_value_inv E Φ v : WP of_val v @ E {{ Φ }} ={E}=★ Φ v.
 Proof.
   rewrite wp_unfold /wp_pre to_of_val. iIntros "[H|[% _]]"; [|done].
   by iDestruct "H" as (v') "[% ?]"; simplify_eq.
@@ -226,7 +226,7 @@ Section proofmode_classes.
   Proof. by rewrite /IsExceptLast -{2}fupd_wp -except_last_fupd -fupd_intro. Qed.
 
   Global Instance elim_upd_bupd_wp E e P Φ :
-    ElimUpd (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+    ElimUpd (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
   Proof. by rewrite /ElimUpd (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
 
   Global Instance elim_upd_fupd_wp E e P Φ :
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 0351fc5bfa91c066839e931b6442c0fdc0109c59..f4d33686a0c36b658e2b6fb813804f74e3c5ab61 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -42,7 +42,7 @@ Implicit Types P : iProp Σ.
 
 (* Allocation *)
 Lemma iris_alloc `{irisPreG Λ Σ} σ :
-  True =r=> ∃ _ : irisG Λ Σ, wsat ★ ownE ⊤ ★ ownP_auth σ ★ ownP σ.
+  True ==★ ∃ _ : irisG Λ Σ, wsat ★ ownE ⊤ ★ ownP_auth σ ★ ownP σ.
 Proof.
   iIntros.
   iUpd (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσ']"; first done.
@@ -65,7 +65,7 @@ Proof.
   rewrite /ownP /ownP_auth own_valid_2 -auth_both_op.
   by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
 Qed.
-Lemma ownP_update σ1 σ2 : ownP_auth σ1 ★ ownP σ1 =r=> ownP_auth σ2 ★ ownP σ2.
+Lemma ownP_update σ1 σ2 : ownP_auth σ1 ★ ownP σ1 ==★ ownP_auth σ2 ★ ownP σ2.
 Proof.
   rewrite /ownP -!own_op.
   by apply own_update, auth_update, option_local_update, exclusive_local_update.
@@ -80,7 +80,7 @@ Qed.
 Global Instance ownI_persistent i P : PersistentP (ownI i P).
 Proof. rewrite /ownI. apply _. Qed.
 
-Lemma ownE_empty : True =r=> ownE ∅.
+Lemma ownE_empty : True ==★ ownE ∅.
 Proof. by rewrite (own_empty (A:=coPset_disjUR) enabled_name). Qed.
 Lemma ownE_op E1 E2 : E1 ⊥ E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ★ ownE E2.
 Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
@@ -95,7 +95,7 @@ Qed.
 Lemma ownE_singleton_twice i : ownE {[i]} ★ ownE {[i]} ⊢ False.
 Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
 
-Lemma ownD_empty : True =r=> ownD ∅.
+Lemma ownD_empty : True ==★ ownD ∅.
 Proof. by rewrite (own_empty (A:=gset_disjUR _) disabled_name). Qed.
 Lemma ownD_op E1 E2 : E1 ⊥ E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ★ ownD E2.
 Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
@@ -151,7 +151,7 @@ Qed.
 
 Lemma ownI_alloc φ P :
   (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
-  wsat ★ ▷ P =r=> ∃ i, ■ (φ i) ★ wsat ★ ownI i P.
+  wsat ★ ▷ P ==★ ∃ i, ■ (φ i) ★ wsat ★ ownI i P.
 Proof.
   iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
   iUpd (own_empty (A:=gset_disjUR positive) disabled_name) as "HE".
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index e7781a3fe54724a52ba83176de166d05734087ff..31c2b04713a8e85a9114287ec2385750ad6a8d9c 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -16,7 +16,7 @@ Global Instance from_assumption_always_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
 Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
 Global Instance from_assumption_bupd p P Q :
-  FromAssumption p P Q → FromAssumption p P (|=r=> Q)%I.
+  FromAssumption p P Q → FromAssumption p P (|==> Q)%I.
 Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
 
 (* IntoPure *)
@@ -40,7 +40,7 @@ Proof.
   rewrite /FromPure. eapply pure_elim; [done|]=> ?.
   rewrite -cmra_valid_intro //. auto with I.
 Qed.
-Global Instance from_pure_bupd P φ : FromPure P φ → FromPure (|=r=> P) φ.
+Global Instance from_pure_bupd P φ : FromPure P φ → FromPure (|==> P) φ.
 Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
 
 (* IntoPersistentP *)
@@ -110,7 +110,7 @@ Proof. apply and_elim_r', impl_wand. Qed.
 Global Instance into_wand_always R P Q : IntoWand R P Q → IntoWand (□ R) P Q.
 Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
 Global Instance into_wand_bupd R P Q :
-  IntoWand R P Q → IntoWand R (|=r=> P) (|=r=> Q) | 100.
+  IntoWand R P Q → IntoWand R (|==> P) (|==> Q) | 100.
 Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite bupd_wand_r. Qed.
 
 (* FromAnd *)
@@ -143,7 +143,7 @@ Global Instance from_sep_later P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
 Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
 Global Instance from_sep_bupd P Q1 Q2 :
-  FromSep P Q1 Q2 → FromSep (|=r=> P) (|=r=> Q1) (|=r=> Q2).
+  FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
 
 Global Instance from_sep_big_sepM
@@ -317,14 +317,14 @@ Global Instance frame_forall {A} R (Φ Ψ : A → uPred M) :
   (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∀ x, Φ x) (∀ x, Ψ x).
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 
-Global Instance frame_bupd R P Q : Frame R P Q → Frame R (|=r=> P) (|=r=> Q).
+Global Instance frame_bupd R P Q : Frame R P Q → Frame R (|==> P) (|==> Q).
 Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
 
 (* FromOr *)
 Global Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
 Proof. done. Qed.
 Global Instance from_or_bupd P Q1 Q2 :
-  FromOr P Q1 Q2 → FromOr (|=r=> P) (|=r=> Q1) (|=r=> Q2).
+  FromOr P Q1 Q2 → FromOr (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromOr=><-. apply or_elim; apply bupd_mono; auto with I. Qed.
 
 (* IntoOr *)
@@ -338,7 +338,7 @@ Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
 Global Instance from_exist_exist {A} (Φ : A → uPred M): FromExist (∃ a, Φ a) Φ.
 Proof. done. Qed.
 Global Instance from_exist_bupd {A} P (Φ : A → uPred M) :
-  FromExist P Φ → FromExist (|=r=> P) (λ a, |=r=> Φ a)%I.
+  FromExist P Φ → FromExist (|==> P) (λ a, |==> Φ a)%I.
 Proof.
   rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
 Qed.
@@ -367,17 +367,17 @@ Global Instance is_except_last_except_last P : IsExceptLast (â—‡ P).
 Proof. by rewrite /IsExceptLast except_last_idemp. Qed.
 Global Instance is_except_last_later P : IsExceptLast (â–· P).
 Proof. by rewrite /IsExceptLast except_last_later. Qed.
-Global Instance is_except_last_bupd P : IsExceptLast P → IsExceptLast (|=r=> P).
+Global Instance is_except_last_bupd P : IsExceptLast P → IsExceptLast (|==> P).
 Proof.
   rewrite /IsExceptLast=> HP.
   by rewrite -{2}HP -(except_last_idemp P) -except_last_bupd -(except_last_intro P).
 Qed.
 
 (* FromUpd *)
-Global Instance from_upd_bupd P : FromUpd (|=r=> P) P.
+Global Instance from_upd_bupd P : FromUpd (|==> P) P.
 Proof. done. Qed.
 
 (* ElimVs *)
-Global Instance elim_upd_bupd_bupd P Q : ElimUpd (|=r=> P) P (|=r=> Q) (|=r=> Q).
+Global Instance elim_upd_bupd_bupd P Q : ElimUpd (|==> P) P (|==> Q) (|==> Q).
 Proof. by rewrite /ElimUpd bupd_frame_r wand_elim_r bupd_trans. Qed.
 End classes.
diff --git a/proofmode/classes.v b/proofmode/classes.v
index 3b9958f515639d9c6d5e2a56efa126958f5235fe..3cc3e6995e7365e4e78c8dffbc6540d4da23902f 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -68,7 +68,7 @@ Global Arguments into_except_last : clear implicits.
 Class IsExceptLast (Q : uPred M) := is_except_last : ◇ Q ⊢ Q.
 Global Arguments is_except_last : clear implicits.
 
-Class FromUpd (P Q : uPred M) := from_upd : (|=r=> Q) ⊢ P.
+Class FromUpd (P Q : uPred M) := from_upd : (|==> Q) ⊢ P.
 Global Arguments from_upd : clear implicits.
 
 Class ElimUpd (P P' : uPred M) (Q Q' : uPred M) :=
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 59177425ff7bfdb91c1cdab826f28de3e08a6680..f2a640bb10996745827e570834b8963ae6b90efd 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -1223,7 +1223,7 @@ Hint Extern 1 (of_envs _ ⊢ _) =>
   | |- _ ⊢ ▷ _ => iNext
   | |- _ ⊢ □ _ => iClear "*"; iAlways
   | |- _ ⊢ ∃ _, _ => iExists _
-  | |- _ ⊢ |=r=> _ => iUpdIntro
+  | |- _ ⊢ |==> _ => iUpdIntro
   end.
 Hint Extern 1 (of_envs _ ⊢ _) =>
   match goal with |- _ ⊢ (_ ∨ _)%I => iLeft end.