From 1014493f563fb267ebe906a9f67025cfd91a3c4e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 7 May 2022 15:46:36 +0200
Subject: [PATCH] make Prop-level BI connectives notation for bi_emp_valid
 (rather than bi_entails)

---
 iris/base_logic/lib/boxes.v           |   2 +-
 iris/base_logic/lib/gen_inv_heap.v    |   2 +-
 iris/base_logic/lib/ghost_map.v       |  10 +--
 iris/base_logic/lib/gset_bij.v        |   2 +-
 iris/base_logic/lib/later_credits.v   |  24 +++---
 iris/base_logic/lib/mono_nat.v        |   4 +-
 iris/base_logic/lib/na_invariants.v   |   2 +-
 iris/base_logic/lib/own.v             |  22 ++---
 iris/base_logic/lib/saved_prop.v      |   2 +-
 iris/bi/big_op.v                      | 120 +++++++++++++-------------
 iris/bi/derived_laws.v                |   8 +-
 iris/bi/interface.v                   |  28 +++---
 iris/bi/lib/atomic.v                  |   6 +-
 iris/bi/lib/fractional.v              |  13 +--
 iris/bi/lib/laterable.v               |  16 ++--
 iris/bi/lib/relations.v               |   4 +-
 iris/bi/monpred.v                     |   8 +-
 iris/bi/plainly.v                     |   6 +-
 iris/bi/updates.v                     | 109 +++++++++++------------
 iris/program_logic/lifting.v          |   2 +-
 iris/program_logic/ownp.v             |   2 +-
 iris/program_logic/total_weakestpre.v |  14 +--
 iris/program_logic/weakestpre.v       |   2 +-
 iris/proofmode/monpred.v              |   6 +-
 iris_deprecated/base_logic/sts.v      |   8 +-
 iris_heap_lang/primitive_laws.v       |   2 +-
 iris_heap_lang/proofmode.v            |  44 +++++-----
 iris_unstable/base_logic/mono_list.v  |   4 +-
 tests/bi_ascii_parsing.ref            |   2 +-
 tests/proofmode.ref                   |   2 +-
 tests/proofmode_iris.ref              |  15 ----
 tests/proofmode_iris.v                |   5 +-
 32 files changed, 244 insertions(+), 252 deletions(-)

diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 3cbbbfb09..ec1163a15 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -86,7 +86,7 @@ Lemma box_own_auth_update Î³ b1 b2 b3 :
   box_own_auth Î³ (â—E b1) âˆ— box_own_auth Î³ (â—¯E b2)
   ==âˆ— box_own_auth Î³ (â—E b3) âˆ— box_own_auth Î³ (â—¯E b3).
 Proof.
-  rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
+  rewrite /box_own_auth -!own_op. iApply own_update. apply prod_update; last done.
   apply excl_auth_update.
 Qed.
 
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 06946752d..949ff543d 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -219,7 +219,7 @@ Section inv_heap.
 
   Lemma inv_mapsto_own_inv l v I : l â†¦_I v -âˆ— l â†¦_I â–¡.
   Proof.
-    apply own_mono, auth_frag_mono. rewrite singleton_included pair_included.
+    iApply own_mono. apply auth_frag_mono. rewrite singleton_included pair_included.
     right. split; [apply: ucmra_unit_least|done].
   Qed.
 
diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index 2ebcbaa93..7110dcbd6 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -242,15 +242,15 @@ Section lemmas.
   Lemma ghost_map_delete {Î³ m k v} :
     ghost_map_auth Î³ 1 m -âˆ— k â†ª[Î³] v ==âˆ— ghost_map_auth Î³ 1 (delete k m).
   Proof.
-    unseal. apply bi.wand_intro_r. rewrite -own_op.
+    unseal. iApply bi.wand_intro_r. rewrite -own_op.
     iApply own_update. apply: gmap_view_delete.
   Qed.
 
   Lemma ghost_map_update {Î³ m k v} w :
     ghost_map_auth Î³ 1 m -âˆ— k â†ª[Î³] v ==âˆ— ghost_map_auth Î³ 1 (<[k := w]> m) âˆ— k â†ª[Î³] w.
   Proof.
-    unseal. apply bi.wand_intro_r. rewrite -!own_op.
-    apply own_update. apply: gmap_view_update.
+    unseal. iApply bi.wand_intro_r. rewrite -!own_op.
+    iApply own_update. apply: gmap_view_update.
   Qed.
 
   (** Big-op versions of above lemmas *)
@@ -270,8 +270,8 @@ Section lemmas.
     ghost_map_auth Î³ 1 m ==âˆ—
     ghost_map_auth Î³ 1 (m' âˆª m) âˆ— ([âˆ— map] k â†¦ v âˆˆ m', k â†ª[Î³] v).
   Proof.
-    unseal. intros ?. rewrite -big_opM_own_1 -own_op.
-    apply own_update. apply: gmap_view_alloc_big; done.
+    unseal. intros ?. rewrite -big_opM_own_1 -own_op. iApply own_update.
+    apply: gmap_view_alloc_big; done.
   Qed.
   Lemma ghost_map_insert_persist_big {Î³ m} m' :
     m' ##â‚˜ m â†’
diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index 4bc86a857..a384b50d1 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -112,7 +112,7 @@ Section gset_bij.
     gset_bij_own_auth Î³ q L -âˆ— gset_bij_own_elem Î³ a b.
   Proof.
     intros. rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
-    by apply own_mono, bij_view_included.
+    iApply own_mono. by apply bij_view_included.
   Qed.
 
   Lemma gset_bij_elem_of {Î³ q L} a b :
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index c7624ac10..7d424f4a9 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -183,13 +183,13 @@ Module le_upd.
       do 9 (done || f_equiv). f_contractive. eapply IH, dist_le; [lia|done|lia].
     Qed.
 
-    Lemma bupd_le_upd P : (|==> P) -âˆ— (|==Â£> P).
+    Lemma bupd_le_upd P : (|==> P) âŠ¢ (|==Â£> P).
     Proof.
       rewrite le_upd_unfold; iIntros "Hupd" (x) "Hpr".
       iMod "Hupd" as "P". iModIntro. iLeft. by iFrame.
     Qed.
 
-    Lemma le_upd_intro P : P -âˆ— |==Â£> P.
+    Lemma le_upd_intro P : P âŠ¢ |==Â£> P.
     Proof.
       iIntros "H"; by iApply bupd_le_upd.
     Qed.
@@ -223,7 +223,7 @@ Module le_upd.
     Qed.
 
     (** Derived lemmas *)
-    Lemma le_upd_mono P Q : (P âŠ¢ Q) â†’ (|==Â£> P) -âˆ— (|==Â£> Q).
+    Lemma le_upd_mono P Q : (P âŠ¢ Q) â†’ (|==Â£> P) âŠ¢ (|==Â£> Q).
     Proof.
       intros Hent. iApply le_upd_bind.
       iIntros "P"; iApply le_upd_intro; by iApply Hent.
@@ -236,16 +236,16 @@ Module le_upd.
     Global Instance le_upd_equiv_proper : Proper ((â‰¡) ==> (â‰¡)) le_upd.
     Proof. apply ne_proper. apply _. Qed.
 
-    Lemma le_upd_trans P :  (|==Â£> |==Â£> P) -âˆ— |==Â£> P.
+    Lemma le_upd_trans P :  (|==Â£> |==Â£> P) âŠ¢ |==Â£> P.
     Proof.
       iIntros "HP". iApply le_upd_bind; eauto.
     Qed.
-    Lemma le_upd_frame_r P R : (|==Â£> P) âˆ— R -âˆ— |==Â£> P âˆ— R.
+    Lemma le_upd_frame_r P R : (|==Â£> P) âˆ— R âŠ¢ |==Â£> P âˆ— R.
     Proof.
       iIntros "[Hupd R]". iApply (le_upd_bind with "[R]"); last done.
       iIntros "P". iApply le_upd_intro. by iFrame.
     Qed.
-    Lemma le_upd_frame_l P R : R âˆ— (|==Â£> P) -âˆ— |==Â£> R âˆ— P.
+    Lemma le_upd_frame_l P R : R âˆ— (|==Â£> P) âŠ¢ |==Â£> R âˆ— P.
     Proof. rewrite comm le_upd_frame_r comm //. Qed.
 
     Lemma le_upd_later P :
@@ -405,7 +405,7 @@ Module le_upd_if.
     Global Instance le_upd_if_ne b : NonExpansive (le_upd_if b).
     Proof. destruct b; apply _. Qed.
 
-    Lemma le_upd_if_intro b P : P -âˆ— le_upd_if b P.
+    Lemma le_upd_if_intro b P : P âŠ¢ le_upd_if b P.
     Proof.
       destruct b; [apply le_upd_intro | apply bupd_intro].
     Qed.
@@ -417,25 +417,25 @@ Module le_upd_if.
       iIntros "HPQ >HP". by iApply "HPQ".
     Qed.
 
-    Lemma le_upd_if_mono b P Q : (P âŠ¢ Q) â†’ (le_upd_if b P) -âˆ— (le_upd_if b Q).
+    Lemma le_upd_if_mono b P Q : (P âŠ¢ Q) â†’ (le_upd_if b P) âŠ¢ (le_upd_if b Q).
     Proof.
       destruct b; [apply le_upd_mono | apply bupd_mono].
     Qed.
-    Lemma le_upd_if_trans b P : (le_upd_if b (le_upd_if b P)) -âˆ— le_upd_if b P.
+    Lemma le_upd_if_trans b P : (le_upd_if b (le_upd_if b P)) âŠ¢ le_upd_if b P.
     Proof.
       destruct b; [apply le_upd_trans | apply bupd_trans].
     Qed.
-    Lemma le_upd_if_frame_r b P R : (le_upd_if b P) âˆ— R -âˆ— le_upd_if b (P âˆ— R).
+    Lemma le_upd_if_frame_r b P R : (le_upd_if b P) âˆ— R âŠ¢ le_upd_if b (P âˆ— R).
     Proof.
       destruct b; [apply le_upd_frame_r | apply bupd_frame_r].
     Qed.
 
-    Lemma bupd_le_upd_if b P : (|==> P) -âˆ— (le_upd_if b P).
+    Lemma bupd_le_upd_if b P : (|==> P) âŠ¢ (le_upd_if b P).
     Proof.
       destruct b; [apply bupd_le_upd | done].
     Qed.
 
-    Lemma le_upd_if_frame_l b R Q : (R âˆ— le_upd_if b Q) -âˆ— le_upd_if b (R âˆ— Q).
+    Lemma le_upd_if_frame_l b R Q : (R âˆ— le_upd_if b Q) âŠ¢ le_upd_if b (R âˆ— Q).
     Proof.
       rewrite comm le_upd_if_frame_r comm //.
     Qed.
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 1242c5314..a6d48fda5 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -90,12 +90,12 @@ Section mono_nat.
   with "Hauth") as "#Hfrag"]. *)
   Lemma mono_nat_lb_own_get Î³ q n :
     mono_nat_auth_own Î³ q n -âˆ— mono_nat_lb_own Î³ n.
-  Proof. unseal. apply own_mono, mono_nat_included. Qed.
+  Proof. unseal. iApply own_mono. apply mono_nat_included. Qed.
 
   Lemma mono_nat_lb_own_le {Î³ n} n' :
     n' â‰¤ n â†’
     mono_nat_lb_own Î³ n -âˆ— mono_nat_lb_own Î³ n'.
-  Proof. unseal. intros. by apply own_mono, mono_nat_lb_mono. Qed.
+  Proof. unseal. intros. iApply own_mono. by apply mono_nat_lb_mono. Qed.
 
   Lemma mono_nat_lb_own_0 Î³ :
     âŠ¢ |==> mono_nat_lb_own Î³ 0.
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index dc72c7ca8..226160a08 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -58,7 +58,7 @@ Section proofs.
 
   Lemma na_own_disjoint p E1 E2 : na_own p E1 -âˆ— na_own p E2 -âˆ— âŒœE1 ## E2âŒ.
   Proof.
-    apply wand_intro_r.
+    iApply wand_intro_r.
     rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
   Qed.
 
diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 71f9f9bcf..2be0458d2 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import functions gmap proofmode_classes.
-From iris.proofmode Require Import classes.
+From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Export iprop.
 From iris.prelude Require Import options.
 Import uPred.
@@ -181,9 +181,9 @@ Proof. intros a1 a2. apply own_mono. Qed.
 Lemma own_valid Î³ a : own Î³ a âŠ¢ âœ“ a.
 Proof. by rewrite !own_eq /own_def ownM_valid iRes_singleton_validI. Qed.
 Lemma own_valid_2 Î³ a1 a2 : own Î³ a1 -âˆ— own Î³ a2 -âˆ— âœ“ (a1 â‹… a2).
-Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
+Proof. apply entails_wand, wand_intro_r. by rewrite -own_op own_valid. Qed.
 Lemma own_valid_3 Î³ a1 a2 a3 : own Î³ a1 -âˆ— own Î³ a2 -âˆ— own Î³ a3 -âˆ— âœ“ (a1 â‹… a2 â‹… a3).
-Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
+Proof. apply entails_wand. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
 Lemma own_valid_r Î³ a : own Î³ a âŠ¢ own Î³ a âˆ— âœ“ a.
 Proof. apply: bi.persistent_entails_r. apply own_valid. Qed.
 Lemma own_valid_l Î³ a : own Î³ a âŠ¢ âœ“ a âˆ— own Î³ a.
@@ -194,7 +194,7 @@ Proof. rewrite !own_eq /own_def. apply _. Qed.
 Global Instance own_core_persistent Î³ a : CoreId a â†’ Persistent (own Î³ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
 
-Lemma later_own Î³ a : â–· own Î³ a -âˆ— â—‡ âˆƒ b, own Î³ b âˆ§ â–· (a â‰¡ b).
+Lemma later_own Î³ a : â–· own Î³ a âŠ¢ â—‡ âˆƒ b, own Î³ b âˆ§ â–· (a â‰¡ b).
 Proof.
   rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
   assert (NonExpansive (Î» r : iResUR Î£, r (inG_id i) !! Î³)).
@@ -256,7 +256,7 @@ Lemma own_alloc a : âœ“ a â†’ âŠ¢ |==> âˆƒ Î³, own Î³ a.
 Proof. intros Ha. eapply (own_alloc_dep (Î» _, a)); eauto. Qed.
 
 (** ** Frame preserving updates *)
-Lemma own_updateP P Î³ a : a ~~>: P â†’ own Î³ a ==âˆ— âˆƒ a', âŒœP a'âŒ âˆ— own Î³ a'.
+Lemma own_updateP P Î³ a : a ~~>: P â†’ own Î³ a âŠ¢ |==> âˆƒ a', âŒœP a'âŒ âˆ— own Î³ a'.
 Proof.
   intros Hupd. rewrite !own_eq.
   rewrite -(bupd_mono (âˆƒ m,
@@ -275,17 +275,19 @@ Proof.
     by apply and_intro; [apply pure_intro|].
 Qed.
 
-Lemma own_update Î³ a a' : a ~~> a' â†’ own Î³ a ==âˆ— 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.
-  apply bupd_mono, exist_elim=> a''. rewrite sep_and. apply pure_elim_l=> -> //.
+  intros. iIntros "?".
+  iMod (own_updateP (a' =.) with "[$]") as (a'') "[-> $]".
+  { by apply cmra_update_updateP. }
+  done.
 Qed.
 Lemma own_update_2 Î³ a1 a2 a' :
   a1 â‹… a2 ~~> a' â†’ own Î³ a1 -âˆ— own Î³ a2 ==âˆ— own Î³ a'.
-Proof. intros. apply wand_intro_r. rewrite -own_op. by apply own_update. Qed.
+Proof. intros. apply entails_wand, wand_intro_r. rewrite -own_op. by iApply own_update. Qed.
 Lemma own_update_3 Î³ a1 a2 a3 a' :
   a1 â‹… a2 â‹… a3 ~~> a' â†’ own Î³ a1 -âˆ— own Î³ a2 -âˆ— own Î³ a3 ==âˆ— own Î³ a'.
-Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. by apply own_update. Qed.
+Proof. intros. apply entails_wand. do 2 apply wand_intro_r. rewrite -!own_op. by iApply own_update. Qed.
 End global.
 
 Global Arguments own_valid {_ _} [_] _ _.
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 1571af345..ec6febac2 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -69,7 +69,7 @@ Section saved_anything.
   Lemma saved_anything_valid Î³ dq x :
     saved_anything_own Î³ dq x -âˆ— âŒœâœ“ dqâŒ.
   Proof.
-    rewrite /saved_anything_own own_valid dfrac_agree_validI //.
+    rewrite /saved_anything_own own_valid dfrac_agree_validI //. eauto.
   Qed.
   Lemma saved_anything_valid_2 Î³ dq1 dq2 x y :
     saved_anything_own Î³ dq1 x -âˆ— saved_anything_own Î³ dq2 y -âˆ— âŒœâœ“ (dq1 â‹… dq2)âŒ âˆ— x â‰¡ y.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 31957e495..ad7d004d3 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -226,7 +226,7 @@ Section sep_list.
     ([âˆ— list] kâ†¦x âˆˆ l, Î¦ k x) -âˆ—
     ([âˆ— list] kâ†¦x âˆˆ l, Î¨ k x) -âˆ—
     ([âˆ— list] kâ†¦x âˆˆ l, Î¦ k x âˆ— Î¨ k x).
-  Proof. apply wand_intro_r. rewrite big_sepL_sep //. Qed.
+  Proof. apply entails_wand, wand_intro_r. rewrite big_sepL_sep //. Qed.
 
   Lemma big_sepL_and Î¦ Î¨ l :
     ([âˆ— list] kâ†¦x âˆˆ l, Î¦ k x âˆ§ Î¨ k x)
@@ -299,7 +299,7 @@ Section sep_list.
     â–¡ (âˆ€ k x, âŒœl !! k = Some xâŒ â†’ Î¦ k x -âˆ— Î¨ k x) -âˆ—
     [âˆ— list] kâ†¦x âˆˆ l, Î¨ k x.
   Proof.
-    apply wand_intro_l. rewrite big_sepL_intro -big_sepL_sep.
+    apply entails_wand, wand_intro_l. rewrite big_sepL_intro -big_sepL_sep.
     by setoid_rewrite wand_elim_l.
   Qed.
 
@@ -308,14 +308,14 @@ Section sep_list.
     ([âˆ— list] kâ†¦x âˆˆ l, Î¦ k x -âˆ— Î¨ k x) -âˆ—
     [âˆ— list] kâ†¦x âˆˆ l, Î¨ k x.
   Proof.
-    apply wand_intro_r. rewrite -big_sepL_sep.
+    apply entails_wand, wand_intro_r. rewrite -big_sepL_sep.
     setoid_rewrite wand_elim_r. done.
   Qed.
 
   Lemma big_sepL_dup P `{!Affine P} l :
     â–¡ (P -âˆ— P âˆ— P) -âˆ— P -âˆ— [âˆ— list] kâ†¦x âˆˆ l, P.
   Proof.
-    apply wand_intro_l.
+    apply entails_wand, wand_intro_l.
     induction l as [|x l IH]=> /=; first by apply: affine.
     rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
     rewrite assoc wand_elim_r -assoc. apply sep_mono; done.
@@ -353,10 +353,11 @@ Section sep_list.
       Î¨ i x -âˆ—
       [âˆ— list] kâ†¦y âˆˆ l, Î¨ k y.
   Proof.
-    intros. rewrite big_sepL_delete //. apply sep_mono_r, forall_intro=> Î¨.
+    intros. apply entails_wand.
+    rewrite big_sepL_delete //. apply sep_mono_r, forall_intro=> Î¨.
     apply wand_intro_r, wand_intro_l.
     rewrite (big_sepL_delete Î¨ l i x) //. apply sep_mono_r.
-    eapply wand_apply; [apply big_sepL_impl|apply sep_mono_r].
+    eapply wand_apply; [apply wand_entails, big_sepL_impl|apply sep_mono_r].
     apply intuitionistically_intro', forall_intro=> k; apply forall_intro=> y.
     apply impl_intro_l, pure_elim_l=> ?; apply wand_intro_r.
     rewrite (forall_elim ) (forall_elim y) pure_True // left_id.
@@ -434,10 +435,10 @@ Section sep_list2.
   Lemma big_sepL2_nil' P `{!Affine P} Î¦ : P âŠ¢ [âˆ— list] kâ†¦y1;y2 âˆˆ [];[], Î¦ k y1 y2.
   Proof. apply: affine. Qed.
   Lemma big_sepL2_nil_inv_l Î¦ l2 :
-    ([âˆ— list] kâ†¦y1;y2 âˆˆ []; l2, Î¦ k y1 y2) -âˆ— âŒœl2 = []âŒ.
+    ([âˆ— list] kâ†¦y1;y2 âˆˆ []; l2, Î¦ k y1 y2) âŠ¢ âŒœl2 = []âŒ.
   Proof. destruct l2; simpl; auto using False_elim, pure_intro. Qed.
   Lemma big_sepL2_nil_inv_r Î¦ l1 :
-    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; [], Î¦ k y1 y2) -âˆ— âŒœl1 = []âŒ.
+    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; [], Î¦ k y1 y2) âŠ¢ âŒœl1 = []âŒ.
   Proof. destruct l1; simpl; auto using False_elim, pure_intro. Qed.
 
   Lemma big_sepL2_cons Î¦ x1 x2 l1 l2 :
@@ -445,7 +446,7 @@ Section sep_list2.
     âŠ£âŠ¢ Î¦ 0 x1 x2 âˆ— [âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¦ (S k) y1 y2.
   Proof. done. Qed.
   Lemma big_sepL2_cons_inv_l Î¦ x1 l1 l2 :
-    ([âˆ— list] kâ†¦y1;y2 âˆˆ x1 :: l1; l2, Î¦ k y1 y2) -âˆ—
+    ([âˆ— list] kâ†¦y1;y2 âˆˆ x1 :: l1; l2, Î¦ k y1 y2) âŠ¢
     âˆƒ x2 l2', âŒœ l2 = x2 :: l2' âŒ âˆ§
               Î¦ 0 x1 x2 âˆ— [âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2', Î¦ (S k) y1 y2.
   Proof.
@@ -453,7 +454,7 @@ Section sep_list2.
     by rewrite -(exist_intro x2) -(exist_intro l2) pure_True // left_id.
   Qed.
   Lemma big_sepL2_cons_inv_r Î¦ x2 l1 l2 :
-    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; x2 :: l2, Î¦ k y1 y2) -âˆ—
+    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; x2 :: l2, Î¦ k y1 y2) âŠ¢
     âˆƒ x1 l1', âŒœ l1 = x1 :: l1' âŒ âˆ§
               Î¦ 0 x1 x2 âˆ— [âˆ— list] kâ†¦y1;y2 âˆˆ l1';l2, Î¦ (S k) y1 y2.
   Proof.
@@ -466,7 +467,7 @@ Section sep_list2.
   Proof. by rewrite /= right_id. Qed.
 
   Lemma big_sepL2_length Î¦ l1 l2 :
-    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; l2, Î¦ k y1 y2) -âˆ— âŒœ length l1 = length l2 âŒ.
+    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; l2, Î¦ k y1 y2) âŠ¢ âŒœ length l1 = length l2 âŒ.
   Proof. by rewrite big_sepL2_alt and_elim_l. Qed.
 
   Lemma big_sepL2_fst_snd Î¦ l :
@@ -478,7 +479,7 @@ Section sep_list2.
   Qed.
 
   Lemma big_sepL2_app Î¦ l1 l2 l1' l2' :
-    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; l1', Î¦ k y1 y2) -âˆ—
+    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; l1', Î¦ k y1 y2) âŠ¢
     ([âˆ— list] kâ†¦y1;y2 âˆˆ l2; l2', Î¦ (length l1 + k) y1 y2) -âˆ—
     ([âˆ— list] kâ†¦y1;y2 âˆˆ l1 ++ l2; l1' ++ l2', Î¦ k y1 y2).
   Proof.
@@ -489,7 +490,7 @@ Section sep_list2.
     - by rewrite -assoc IH.
   Qed.
   Lemma big_sepL2_app_inv_l Î¦ l1' l1'' l2 :
-    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1' ++ l1''; l2, Î¦ k y1 y2) -âˆ—
+    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1' ++ l1''; l2, Î¦ k y1 y2) âŠ¢
     âˆƒ l2' l2'', âŒœ l2 = l2' ++ l2'' âŒ âˆ§
                 ([âˆ— list] kâ†¦y1;y2 âˆˆ l1';l2', Î¦ k y1 y2) âˆ—
                 ([âˆ— list] kâ†¦y1;y2 âˆˆ l1'';l2'', Î¦ (length l1' + k) y1 y2).
@@ -501,7 +502,7 @@ Section sep_list2.
     by rewrite IH -assoc.
   Qed.
   Lemma big_sepL2_app_inv_r Î¦ l1 l2' l2'' :
-    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; l2' ++ l2'', Î¦ k y1 y2) -âˆ—
+    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; l2' ++ l2'', Î¦ k y1 y2) âŠ¢
     âˆƒ l1' l1'', âŒœ l1 = l1' ++ l1'' âŒ âˆ§
                 ([âˆ— list] kâ†¦y1;y2 âˆˆ l1';l2', Î¦ k y1 y2) âˆ—
                 ([âˆ— list] kâ†¦y1;y2 âˆˆ l1'';l2'', Î¦ (length l2' + k) y1 y2).
@@ -514,7 +515,7 @@ Section sep_list2.
   Qed.
   Lemma big_sepL2_app_inv Î¦ l1 l2 l1' l2' :
     length l1 = length l1' âˆ¨ length l2 = length l2' â†’
-    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1 ++ l2; l1' ++ l2', Î¦ k y1 y2) -âˆ—
+    ([âˆ— list] kâ†¦y1;y2 âˆˆ l1 ++ l2; l1' ++ l2', Î¦ k y1 y2) âŠ¢
     ([âˆ— list] kâ†¦y1;y2 âˆˆ l1; l1', Î¦ k y1 y2) âˆ—
     ([âˆ— list] kâ†¦y1;y2 âˆˆ l2; l2', Î¦ (length l1 + k)%nat y1 y2).
   Proof.
@@ -534,7 +535,7 @@ Section sep_list2.
   Proof.
     intros. apply (anti_symm _).
     - by apply big_sepL2_app_inv.
-    - apply wand_elim_l'. apply big_sepL2_app.
+    - apply wand_elim_l', big_sepL2_app.
   Qed.
 
   Lemma big_sepL2_snoc Î¦ x1 x2 l1 l2 :
@@ -707,7 +708,7 @@ Section sep_list2.
     ([âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¦ k y1 y2) -âˆ—
     ([âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¨ k y1 y2) -âˆ—
     ([âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¦ k y1 y2 âˆ— Î¨ k y1 y2).
-  Proof. apply wand_intro_r. rewrite big_sepL2_sep //. Qed.
+  Proof. apply entails_wand, wand_intro_r. rewrite big_sepL2_sep //. Qed.
 
   Lemma big_sepL2_and Î¦ Î¨ l1 l2 :
     ([âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¦ k y1 y2 âˆ§ Î¨ k y1 y2)
@@ -798,7 +799,7 @@ Section sep_list2.
       âŒœl1 !! k = Some x1âŒ â†’ âŒœl2 !! k = Some x2âŒ â†’ Î¦ k x1 x2 -âˆ— Î¨ k x1 x2) -âˆ—
     [âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¨ k y1 y2.
   Proof.
-    rewrite -(idemp bi_and (big_sepL2 _ _ _)) {1}big_sepL2_length.
+    apply entails_wand. rewrite -(idemp bi_and (big_sepL2 _ _ _)) {1}big_sepL2_length.
     apply pure_elim_l=> ?. rewrite big_sepL2_intro //.
     apply bi.wand_intro_l. rewrite -big_sepL2_sep. by setoid_rewrite wand_elim_l.
   Qed.
@@ -808,7 +809,7 @@ Section sep_list2.
     ([âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¦ k y1 y2 -âˆ— Î¨ k y1 y2) -âˆ—
     [âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¨ k y1 y2.
   Proof.
-    apply wand_intro_r. rewrite -big_sepL2_sep.
+    apply entails_wand, wand_intro_r. rewrite -big_sepL2_sep.
     setoid_rewrite wand_elim_r. done.
   Qed.
 
@@ -850,10 +851,10 @@ Section sep_list2.
       Î¨ i x1 x2 -âˆ—
       [âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¨ k y1 y2.
   Proof.
-    intros. rewrite big_sepL2_delete //. apply sep_mono_r, forall_intro=> Î¨.
+    intros. rewrite big_sepL2_delete //. apply entails_wand, sep_mono_r, forall_intro=> Î¨.
     apply wand_intro_r, wand_intro_l.
     rewrite (big_sepL2_delete Î¨ l1 l2 i) //. apply sep_mono_r.
-    eapply wand_apply; [apply big_sepL2_impl|apply sep_mono_r].
+    eapply wand_apply; [apply wand_entails, big_sepL2_impl|apply sep_mono_r].
     apply intuitionistically_intro', forall_intro=> k;
       apply forall_intro=> y1; apply forall_intro=> y2.
     do 2 (apply impl_intro_l, pure_elim_l=> ?); apply wand_intro_r.
@@ -903,7 +904,7 @@ Section sep_list2.
     ([âˆ— list] kâ†¦y1 âˆˆ l1, Î¦1 k y1) -âˆ—
     ([âˆ— list] kâ†¦y2 âˆˆ l2, Î¦2 k y2) -âˆ—
     [âˆ— list] kâ†¦y1;y2 âˆˆ l1;l2, Î¦1 k y1 âˆ— Î¦2 k y2.
-  Proof. intros. apply wand_intro_r. by rewrite big_sepL2_sepL. Qed.
+  Proof. intros. apply entails_wand, wand_intro_r. by rewrite big_sepL2_sepL. Qed.
 End sep_list2.
 
 Lemma big_sepL2_const_sepL_l {A B} (Î¦ : nat â†’ A â†’ PROP) (l1 : list A) (l2 : list B) :
@@ -946,7 +947,7 @@ Proof.
 Qed.
 
 Lemma big_sepL_sepL2_diag {A} (Î¦ : nat â†’ A â†’ A â†’ PROP) (l : list A) :
-  ([âˆ— list] kâ†¦y âˆˆ l, Î¦ k y y) -âˆ—
+  ([âˆ— list] kâ†¦y âˆˆ l, Î¦ k y y) âŠ¢
   ([âˆ— list] kâ†¦y1;y2 âˆˆ l;l, Î¦ k y1 y2).
 Proof.
   rewrite big_sepL2_alt. rewrite pure_True // left_id.
@@ -1091,7 +1092,7 @@ Section and_list.
 
   Lemma big_andL_impl Î¦ Î¨ m :
     ([âˆ§ list] kâ†¦x âˆˆ m, Î¦ k x) âˆ§
-    (âˆ€ k x, âŒœm !! k = Some xâŒ â†’ Î¦ k x â†’ Î¨ k x) -âˆ—
+    (âˆ€ k x, âŒœm !! k = Some xâŒ â†’ Î¦ k x â†’ Î¨ k x) âŠ¢
     [âˆ§ list] kâ†¦x âˆˆ m, Î¨ k x.
   Proof.
     rewrite -big_andL_forall -big_andL_and.
@@ -1362,7 +1363,7 @@ Section sep_map.
 
   Lemma big_sepM_insert_2 Î¦ m i x
     `{!TCOr (âˆ€ y, Affine (Î¦ i y)) (Absorbing (Î¦ i x))} :
-    Î¦ i x -âˆ— ([âˆ— map] kâ†¦y âˆˆ m, Î¦ k y) -âˆ— [âˆ— map] kâ†¦y âˆˆ <[i:=x]> m, Î¦ k y.
+    Î¦ i x âŠ¢ ([âˆ— map] kâ†¦y âˆˆ m, Î¦ k y) -âˆ— [âˆ— map] kâ†¦y âˆˆ <[i:=x]> m, Î¦ k y.
   Proof.
     apply wand_intro_r. destruct (m !! i) as [y|] eqn:Hi; last first.
     { by rewrite -big_sepM_insert. }
@@ -1477,7 +1478,7 @@ Section sep_map.
     ([âˆ— map] kâ†¦x âˆˆ m, Î¦ k x) -âˆ—
     ([âˆ— map] kâ†¦x âˆˆ m, Î¨ k x) -âˆ—
     ([âˆ— map] kâ†¦x âˆˆ m, Î¦ k x âˆ— Î¨ k x).
-  Proof. apply wand_intro_r. rewrite big_sepM_sep //. Qed.
+  Proof. apply entails_wand, wand_intro_r. rewrite big_sepM_sep //. Qed.
 
   Lemma big_sepM_and Î¦ Î¨ m :
     ([âˆ— map] kâ†¦x âˆˆ m, Î¦ k x âˆ§ Î¨ k x)
@@ -1550,7 +1551,7 @@ Section sep_map.
     â–¡ (âˆ€ k x, âŒœm !! k = Some xâŒ â†’ Î¦ k x -âˆ— Î¨ k x) -âˆ—
     [âˆ— map] kâ†¦x âˆˆ m, Î¨ k x.
   Proof.
-    apply wand_intro_l. rewrite big_sepM_intro -big_sepM_sep.
+    apply entails_wand, wand_intro_l. rewrite big_sepM_intro -big_sepM_sep.
     by setoid_rewrite wand_elim_l.
   Qed.
 
@@ -1559,14 +1560,14 @@ Section sep_map.
     ([âˆ— map] kâ†¦x âˆˆ m, Î¦ k x -âˆ— Î¨ k x) -âˆ—
     [âˆ— map] kâ†¦x âˆˆ m, Î¨ k x.
   Proof.
-    apply wand_intro_r. rewrite -big_sepM_sep.
+    apply entails_wand, wand_intro_r. rewrite -big_sepM_sep.
     setoid_rewrite wand_elim_r. done.
   Qed.
 
   Lemma big_sepM_dup P `{!Affine P} m :
     â–¡ (P -âˆ— P âˆ— P) -âˆ— P -âˆ— [âˆ— map] kâ†¦x âˆˆ m, P.
   Proof.
-    apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
+    apply entails_wand, wand_intro_l. induction m as [|i x m ? IH] using map_ind.
     { apply: big_sepM_empty'. }
     rewrite !big_sepM_insert //.
     rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
@@ -1584,10 +1585,10 @@ Section sep_map.
       Î¨ i x -âˆ—
       [âˆ— map] kâ†¦y âˆˆ m, Î¨ k y.
   Proof.
-    intros. rewrite big_sepM_delete //. apply sep_mono_r, forall_intro=> Î¨.
+    intros. rewrite big_sepM_delete //. apply entails_wand, sep_mono_r, forall_intro=> Î¨.
     apply wand_intro_r, wand_intro_l.
     rewrite (big_sepM_delete Î¨ m i x) //. apply sep_mono_r.
-    eapply wand_apply; [apply big_sepM_impl|apply sep_mono_r].
+    eapply wand_apply; [apply wand_entails, big_sepM_impl|apply sep_mono_r].
     f_equiv; f_equiv=> k; f_equiv=> y.
     rewrite impl_curry -pure_and lookup_delete_Some.
     do 2 f_equiv. intros ?; naive_solver.
@@ -1637,7 +1638,7 @@ Proof. apply big_opM_sep_zip. Qed.
 
 Lemma big_sepM_impl_strong `{Countable K} {A B}
     (Î¦ : K â†’ A â†’ PROP) (Î¨ : K â†’ B â†’ PROP) (m1 : gmap K A) (m2 : gmap K B) :
-  ([âˆ— map] kâ†¦x âˆˆ m1, Î¦ k x) -âˆ—
+  ([âˆ— map] kâ†¦x âˆˆ m1, Î¦ k x) âŠ¢
   â–¡ (âˆ€ (k : K) (y : B),
     (if m1 !! k is Some x then Î¦ k x else emp) -âˆ—
     âŒœm2 !! k = Some yâŒ â†’
@@ -1687,7 +1688,7 @@ Lemma big_sepM_impl_dom_subseteq `{Countable K} {A B}
   ([âˆ— map] kâ†¦y âˆˆ m2, Î¨ k y) âˆ—
   ([âˆ— map] kâ†¦x âˆˆ filter (Î» '(k, _), m2 !! k = None) m1, Î¦ k x).
 Proof.
-  intros. rewrite big_sepM_impl_strong.
+  intros. apply entails_wand. rewrite big_sepM_impl_strong.
   apply wand_mono; last done. f_equiv. f_equiv=> k. apply forall_intro=> y.
   apply wand_intro_r, impl_intro_l, pure_elim_l=> Hlm2.
   destruct (m1 !! k) as [x|] eqn:Hlm1.
@@ -1772,7 +1773,7 @@ Section and_map.
   Proof. apply big_opM_insert_delete. Qed.
 
   Lemma big_andM_insert_2 Î¦ m i x :
-    Î¦ i x âˆ§ ([âˆ§ map] kâ†¦y âˆˆ m, Î¦ k y) -âˆ— [âˆ§ map] kâ†¦y âˆˆ <[i:=x]> m, Î¦ k y.
+    Î¦ i x âˆ§ ([âˆ§ map] kâ†¦y âˆˆ m, Î¦ k y) âŠ¢ [âˆ§ map] kâ†¦y âˆˆ <[i:=x]> m, Î¦ k y.
   Proof.
     rewrite big_andM_insert_delete.
     destruct (m !! i) eqn:Hi; [ | by rewrite delete_notin ].
@@ -1861,7 +1862,7 @@ Section and_map.
 
   Lemma big_andM_impl Î¦ Î¨ m :
     ([âˆ§ map] kâ†¦x âˆˆ m, Î¦ k x) âˆ§
-    (âˆ€ k x, âŒœm !! k = Some xâŒ â†’ Î¦ k x â†’ Î¨ k x) -âˆ—
+    (âˆ€ k x, âŒœm !! k = Some xâŒ â†’ Î¦ k x â†’ Î¨ k x) âŠ¢
     [âˆ§ map] kâ†¦x âˆˆ m, Î¨ k x.
   Proof.
     rewrite -big_andM_forall -big_andM_and.
@@ -2152,7 +2153,7 @@ Section map2.
     rewrite !big_sepM2_alt.
     assert (TCOr (âˆ€ x, Affine (Î¦ i x.1 x.2)) (Absorbing (Î¦ i x1 x2))).
     { destruct select (TCOr _ _); apply _. }
-    apply wand_intro_r.
+    apply entails_wand, wand_intro_r.
     rewrite !persistent_and_affinely_sep_l /=.
     rewrite (sep_comm  (Î¦ _ _ _)) -sep_assoc. apply sep_mono.
     { apply affinely_mono, pure_mono. intros Hm k.
@@ -2258,7 +2259,7 @@ Section map2.
     ([âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¦ k y1 y2) -âˆ—
     ([âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¨ k y1 y2) -âˆ—
     ([âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¦ k y1 y2 âˆ— Î¨ k y1 y2).
-  Proof. apply wand_intro_r. rewrite big_sepM2_sep //. Qed.
+  Proof. apply entails_wand, wand_intro_r. rewrite big_sepM2_sep //. Qed.
 
   Lemma big_sepM2_and Î¦ Î¨ m1 m2 :
     ([âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¦ k y1 y2 âˆ§ Î¨ k y1 y2)
@@ -2351,6 +2352,7 @@ Section map2.
       âŒœm1 !! k = Some x1âŒ â†’ âŒœm2 !! k = Some x2âŒ â†’ Î¦ k x1 x2 -âˆ— Î¨ k x1 x2) -âˆ—
     [âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¨ k y1 y2.
   Proof.
+    apply entails_wand.
     rewrite -(idemp bi_and (big_sepM2 _ _ _)) {1}big_sepM2_lookup_iff.
     apply pure_elim_l=> ?. rewrite big_sepM2_intro //.
     apply bi.wand_intro_l. rewrite -big_sepM2_sep. by setoid_rewrite wand_elim_l.
@@ -2361,7 +2363,7 @@ Section map2.
     ([âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¦ k y1 y2 -âˆ— Î¨ k y1 y2) -âˆ—
     [âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¨ k y1 y2.
   Proof.
-    apply wand_intro_r. rewrite -big_sepM2_sep.
+    apply entails_wand, wand_intro_r. rewrite -big_sepM2_sep.
     setoid_rewrite wand_elim_r. done.
   Qed.
 
@@ -2379,10 +2381,10 @@ Section map2.
       Î¨ i x1 x2 -âˆ—
       [âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¨ k y1 y2.
   Proof.
-    intros. rewrite big_sepM2_delete //. apply sep_mono_r, forall_intro=> Î¨.
+    intros. rewrite big_sepM2_delete //. apply entails_wand, sep_mono_r, forall_intro=> Î¨.
     apply wand_intro_r, wand_intro_l.
     rewrite (big_sepM2_delete Î¨ m1 m2 i) //. apply sep_mono_r.
-    eapply wand_apply; [apply big_sepM2_impl|apply sep_mono_r].
+    eapply wand_apply; [apply wand_entails, big_sepM2_impl|apply sep_mono_r].
     f_equiv; f_equiv=> k; f_equiv=> y1; f_equiv=> y2.
     rewrite !impl_curry -!pure_and !lookup_delete_Some.
     do 2 f_equiv. intros ?; naive_solver.
@@ -2425,7 +2427,7 @@ Section map2.
     ([âˆ— map] kâ†¦y1 âˆˆ m1, Î¦1 k y1) -âˆ—
     ([âˆ— map] kâ†¦y2 âˆˆ m2, Î¦2 k y2) -âˆ—
     [âˆ— map] kâ†¦y1;y2 âˆˆ m1;m2, Î¦1 k y1 âˆ— Î¦2 k y2.
-  Proof. intros. apply wand_intro_r. by rewrite big_sepM2_sepM. Qed.
+  Proof. intros. apply entails_wand, wand_intro_r. by rewrite big_sepM2_sepM. Qed.
 
  Lemma big_sepM2_union_inv_l (Î¦ : K â†’ A â†’ B â†’ PROP) m1 m2 m' :
     m1 ##â‚˜ m2 â†’
@@ -2472,7 +2474,7 @@ Proof.
 Qed.
 
 Lemma big_sepM_sepM2_diag `{Countable K} {A} (Î¦ : K â†’ A â†’ A â†’ PROP) (m : gmap K A) :
-  ([âˆ— map] kâ†¦y âˆˆ m, Î¦ k y y) -âˆ—
+  ([âˆ— map] kâ†¦y âˆˆ m, Î¦ k y y) âŠ¢
   ([âˆ— map] kâ†¦y1;y2 âˆˆ m;m, Î¦ k y1 y2).
 Proof.
   rewrite big_sepM2_alt. rewrite pure_True; last naive_solver. rewrite left_id.
@@ -2601,7 +2603,7 @@ Section gset.
 
   Lemma big_sepS_insert_2 {Î¦ X} x
     `{!TCOr (Affine (Î¦ x)) (Absorbing (Î¦ x))} :
-    Î¦ x -âˆ— ([âˆ— set] y âˆˆ X, Î¦ y) -âˆ— ([âˆ— set] y âˆˆ {[ x ]} âˆª X, Î¦ y).
+    Î¦ x âŠ¢ ([âˆ— set] y âˆˆ X, Î¦ y) -âˆ— ([âˆ— set] y âˆˆ {[ x ]} âˆª X, Î¦ y).
   Proof.
     apply wand_intro_r. destruct (decide (x âˆˆ X)); last first.
     { rewrite -big_sepS_insert //. }
@@ -2614,13 +2616,13 @@ Section gset.
   Lemma big_sepS_insert_2' {Î¦ X} x
     `{!TCOr (Affine (Î¦ x)) (Absorbing (Î¦ x))} :
     Î¦ x -âˆ— ([âˆ— set] y âˆˆ X, Î¦ y) -âˆ— ([âˆ— set] y âˆˆ X âˆª {[ x ]}, Î¦ y).
-  Proof. rewrite comm_L. by apply big_sepS_insert_2. Qed.
+  Proof. apply entails_wand. rewrite comm_L. by apply big_sepS_insert_2. Qed.
 
   Lemma big_sepS_union_2 {Î¦} X Y
     `{!âˆ€ x, TCOr (Affine (Î¦ x)) (Absorbing (Î¦ x))} :
     ([âˆ— set] y âˆˆ X, Î¦ y) -âˆ— ([âˆ— set] y âˆˆ Y, Î¦ y) -âˆ— ([âˆ— set] y âˆˆ X âˆª Y, Î¦ y).
   Proof.
-    apply wand_intro_r. induction X as [|x X ? IH] using set_ind_L.
+    apply entails_wand, wand_intro_r. induction X as [|x X ? IH] using set_ind_L.
     { by rewrite left_id_L big_sepS_empty left_id. }
     rewrite big_sepS_insert // -assoc IH -assoc_L.
     destruct (decide (x âˆˆ Y)).
@@ -2632,7 +2634,7 @@ Section gset.
 
   Lemma big_sepS_delete_2 {Î¦ X} x :
     Affine (Î¦ x) â†’
-    Î¦ x -âˆ— ([âˆ— set] y âˆˆ X âˆ– {[ x ]}, Î¦ y) -âˆ— [âˆ— set] y âˆˆ X, Î¦ y.
+    Î¦ x âŠ¢ ([âˆ— set] y âˆˆ X âˆ– {[ x ]}, Î¦ y) -âˆ— [âˆ— set] y âˆˆ X, Î¦ y.
   Proof.
     intros Haff. apply wand_intro_r. destruct (decide (x âˆˆ X)).
     { rewrite -big_sepS_delete //. }
@@ -2677,7 +2679,7 @@ Section gset.
     intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter Ï† Y) X))
       as (Z&->&?); first set_solver.
     rewrite big_sepS_union // big_sepS_filter'.
-    by apply sep_mono_r, wand_intro_l.
+    by apply entails_wand, sep_mono_r, wand_intro_l.
   Qed.
   Lemma big_sepS_filter_acc `{!BiAffine PROP}
       (Ï† : A â†’ Prop) `{âˆ€ y, Decision (Ï† y)} Î¦ X Y :
@@ -2700,7 +2702,7 @@ Section gset.
     ([âˆ— set] y âˆˆ X, Î¦ y) -âˆ—
     ([âˆ— set] y âˆˆ X, Î¨ y) -âˆ—
     ([âˆ— set] y âˆˆ X, Î¦ y âˆ— Î¨ y).
-  Proof. apply wand_intro_r. rewrite big_sepS_sep //. Qed.
+  Proof. apply entails_wand, wand_intro_r. rewrite big_sepS_sep //. Qed.
 
   Lemma big_sepS_and Î¦ Î¨ X :
     ([âˆ— set] y âˆˆ X, Î¦ y âˆ§ Î¨ y) âŠ¢ ([âˆ— set] y âˆˆ X, Î¦ y) âˆ§ ([âˆ— set] y âˆˆ X, Î¨ y).
@@ -2774,7 +2776,7 @@ Section gset.
     â–¡ (âˆ€ x, âŒœx âˆˆ XâŒ â†’ Î¦ x -âˆ— Î¨ x) -âˆ—
     [âˆ— set] x âˆˆ X, Î¨ x.
   Proof.
-    apply wand_intro_l. rewrite big_sepS_intro -big_sepS_sep.
+    apply entails_wand, wand_intro_l. rewrite big_sepS_intro -big_sepS_sep.
     by setoid_rewrite wand_elim_l.
   Qed.
 
@@ -2783,7 +2785,7 @@ Section gset.
     ([âˆ— set] x âˆˆ X, Î¦ x -âˆ— Î¨ x) -âˆ—
     [âˆ— set] x âˆˆ X, Î¨ x.
   Proof.
-    apply wand_intro_r. rewrite -big_sepS_sep.
+    apply entails_wand, wand_intro_r. rewrite -big_sepS_sep.
     setoid_rewrite wand_elim_r. done.
   Qed.
 
@@ -2798,10 +2800,10 @@ Section gset.
       Î¨ x -âˆ—
       [âˆ— set] y âˆˆ X, Î¨ y.
   Proof.
-    intros. rewrite big_sepS_delete //. apply sep_mono_r, forall_intro=> Î¨.
+    intros. rewrite big_sepS_delete //. apply entails_wand, sep_mono_r, forall_intro=> Î¨.
     apply wand_intro_r, wand_intro_l.
     rewrite (big_sepS_delete Î¨ X x) //. apply sep_mono_r.
-    eapply wand_apply; [apply big_sepS_impl|apply sep_mono_r].
+    eapply wand_apply; [apply wand_entails, big_sepS_impl|apply sep_mono_r].
     f_equiv; f_equiv=> y. rewrite impl_curry -pure_and.
     do 2 f_equiv. intros ?; set_solver.
   Qed.
@@ -2809,7 +2811,7 @@ Section gset.
   Lemma big_sepS_dup P `{!Affine P} X :
     â–¡ (P -âˆ— P âˆ— P) -âˆ— P -âˆ— [âˆ— set] x âˆˆ X, P.
   Proof.
-    apply wand_intro_l. induction X as [|x X ? IH] using set_ind_L.
+    apply entails_wand, wand_intro_l. induction X as [|x X ? IH] using set_ind_L.
     { apply: big_sepS_empty'. }
     rewrite !big_sepS_insert //.
     rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
@@ -2946,7 +2948,7 @@ Section gmultiset.
     ([âˆ— mset] y âˆˆ X, Î¦ y) -âˆ—
     ([âˆ— mset] y âˆˆ X, Î¨ y) -âˆ—
     ([âˆ— mset] y âˆˆ X, Î¦ y âˆ— Î¨ y).
-  Proof. apply wand_intro_r. rewrite big_sepMS_sep //. Qed.
+  Proof. apply entails_wand, wand_intro_r. rewrite big_sepMS_sep //. Qed.
 
   Lemma big_sepMS_and Î¦ Î¨ X :
     ([âˆ— mset] y âˆˆ X, Î¦ y âˆ§ Î¨ y) âŠ¢ ([âˆ— mset] y âˆˆ X, Î¦ y) âˆ§ ([âˆ— mset] y âˆˆ X, Î¨ y).
@@ -3036,7 +3038,7 @@ Section gmultiset.
     â–¡ (âˆ€ x, âŒœx âˆˆ XâŒ â†’ Î¦ x -âˆ— Î¨ x) -âˆ—
     [âˆ— mset] x âˆˆ X, Î¨ x.
   Proof.
-    apply wand_intro_l. rewrite big_sepMS_intro -big_sepMS_sep.
+    apply entails_wand, wand_intro_l. rewrite big_sepMS_intro -big_sepMS_sep.
     by setoid_rewrite wand_elim_l.
   Qed.
 
@@ -3045,14 +3047,14 @@ Section gmultiset.
     ([âˆ— mset] x âˆˆ X, Î¦ x -âˆ— Î¨ x) -âˆ—
     [âˆ— mset] x âˆˆ X, Î¨ x.
   Proof.
-    apply wand_intro_r. rewrite -big_sepMS_sep.
+    apply entails_wand, wand_intro_r. rewrite -big_sepMS_sep.
     setoid_rewrite wand_elim_r. done.
   Qed.
 
   Lemma big_sepMS_dup P `{!Affine P} X :
     â–¡ (P -âˆ— P âˆ— P) -âˆ— P -âˆ— [âˆ— mset] x âˆˆ X, P.
   Proof.
-    apply wand_intro_l. induction X as [|x X IH] using gmultiset_ind.
+    apply entails_wand, wand_intro_l. induction X as [|x X IH] using gmultiset_ind.
     { apply: big_sepMS_empty'. }
     rewrite !big_sepMS_disj_union big_sepMS_singleton.
     rewrite intuitionistically_sep_dup {1}intuitionistically_elim.
@@ -3070,10 +3072,10 @@ Section gmultiset.
       Î¨ x -âˆ—
       [âˆ— mset] y âˆˆ X, Î¨ y.
   Proof.
-    intros. rewrite big_sepMS_delete //. apply sep_mono_r, forall_intro=> Î¨.
+    intros. rewrite big_sepMS_delete //. apply entails_wand, sep_mono_r, forall_intro=> Î¨.
     apply wand_intro_r, wand_intro_l.
     rewrite (big_sepMS_delete Î¨ X x) //. apply sep_mono_r.
-    apply wand_elim_l', big_sepMS_impl.
+    apply wand_elim_l', wand_entails, big_sepMS_impl.
   Qed.
 End gmultiset.
 
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 9af410500..4774449d8 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -519,7 +519,7 @@ Qed.
 Lemma and_parallel P1 P2 Q1 Q2 :
   (P1 âˆ§ P2) -âˆ— ((P1 -âˆ— Q1) âˆ§ (P2 -âˆ— Q2)) -âˆ— Q1 âˆ§ Q2.
 Proof.
-  apply wand_intro_r, and_intro.
+  apply entails_wand, wand_intro_r, and_intro.
   - rewrite !and_elim_l wand_elim_r. done.
   - rewrite !and_elim_r wand_elim_r. done.
 Qed.
@@ -1727,15 +1727,15 @@ Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 (* iterated modalities *)
 Lemma iter_modal_intro (M : PROP â†’ PROP) P (n : nat) :
   (âˆ€ Q, Q âŠ¢ M Q) â†’
-  P -âˆ— Nat.iter n M P.
+  P âŠ¢ Nat.iter n M P.
 Proof.
   intros Hintro; induction n as [|n IHn]; simpl; first done.
   etransitivity; first apply IHn. apply Hintro.
 Qed.
 
 Lemma iter_modal_mono (M : PROP â†’ PROP) P Q (n : nat) :
-  (âˆ€ P Q, (P -âˆ— Q) -âˆ— M P -âˆ— M Q)  â†’
-  (P -âˆ— Q) -âˆ—
+  (âˆ€ P Q, (P -âˆ— Q) âŠ¢ M P -âˆ— M Q) â†’
+  (P -âˆ— Q) âŠ¢
   Nat.iter n M P -âˆ— Nat.iter n M Q.
 Proof.
   intros Hmono; induction n as [|n IHn]; simpl; first done.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index f2108ee94..c751e3016 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -246,20 +246,6 @@ Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
 Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) | 170 := {}.
 Global Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
 
-Notation "P âŠ¢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
-Notation "P 'âŠ¢@{' PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) (only parsing) : stdpp_scope.
-Notation "(âŠ¢)" := bi_entails (only parsing) : stdpp_scope.
-Notation "'(âŠ¢@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
-
-Notation "P âŠ£âŠ¢ Q" := (equiv (A:=bi_car _) P%I Q%I) : stdpp_scope.
-Notation "P 'âŠ£âŠ¢@{' PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) (only parsing) : stdpp_scope.
-Notation "(âŠ£âŠ¢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
-Notation "'(âŠ£âŠ¢@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
-Notation "( P âŠ£âŠ¢.)" := (equiv (A:=bi_car _) P) (only parsing) : stdpp_scope.
-Notation "(.âŠ£âŠ¢ Q )" := (Î» P, P â‰¡@{bi_car _} Q) (only parsing) : stdpp_scope.
-
-Notation "P -âˆ— Q" := (P âŠ¢ Q) : stdpp_scope.
-
 Notation "'emp'" := (bi_emp) : bi_scope.
 Notation "'âŒœ' Ï† 'âŒ'" := (bi_pure Ï†%type%stdpp) : bi_scope.
 Notation "'True'" := (bi_pure True) : bi_scope.
@@ -281,6 +267,18 @@ Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
 
 Notation "â–· P" := (bi_later P) : bi_scope.
 
+Notation "P âŠ¢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
+Notation "P 'âŠ¢@{' PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) (only parsing) : stdpp_scope.
+Notation "(âŠ¢)" := bi_entails (only parsing) : stdpp_scope.
+Notation "'(âŠ¢@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
+
+Notation "P âŠ£âŠ¢ Q" := (equiv (A:=bi_car _) P%I Q%I) : stdpp_scope.
+Notation "P 'âŠ£âŠ¢@{' PROP } Q" := (equiv (A:=bi_car PROP) P%I Q%I) (only parsing) : stdpp_scope.
+Notation "(âŠ£âŠ¢)" := (equiv (A:=bi_car _)) (only parsing) : stdpp_scope.
+Notation "'(âŠ£âŠ¢@{' PROP } )" := (equiv (A:=bi_car PROP)) (only parsing) : stdpp_scope.
+Notation "( P âŠ£âŠ¢.)" := (equiv (A:=bi_car _) P) (only parsing) : stdpp_scope.
+Notation "(.âŠ£âŠ¢ Q )" := (Î» P, P â‰¡@{bi_car _} Q) (only parsing) : stdpp_scope.
+
 Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp âŠ¢ P.
 
 Global Arguments bi_emp_valid {_} _%I : simpl never.
@@ -293,6 +291,8 @@ Notation "'(âŠ¢@{' PROP } Q )" := (bi_emp_valid (PROP:=PROP) Q%I) (only parsing)
 Notation "(.âŠ¢ Q )" := (Î» P, P âŠ¢ Q) (only parsing) : stdpp_scope.
 Notation "( P âŠ¢.)" := (bi_entails P) (only parsing) : stdpp_scope.
 
+Notation "P -âˆ— Q" := (âŠ¢ P -âˆ— Q) : stdpp_scope.
+
 Module bi.
 Section bi_laws.
 Context {PROP : bi}.
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index b37df02b9..3ac2c2a09 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -247,7 +247,7 @@ Section lemmas.
 
   (** The elimination form: an atomic accessor *)
   Lemma aupd_aacc Eo Ei Î± Î² Î¦ :
-    atomic_update Eo Ei Î± Î² Î¦ -âˆ—
+    atomic_update Eo Ei Î± Î² Î¦ âŠ¢
     atomic_acc Eo Ei Î± (atomic_update Eo Ei Î± Î² Î¦) Î² Î¦.
   Proof using Type*. by rewrite {1}aupd_unfold. Qed.
 
@@ -271,8 +271,8 @@ Section lemmas.
   directly; use the [iAuIntro] tactic instead. *)
   Local Lemma aupd_intro P Q Î± Î² Eo Ei Î¦ :
     Absorbing P â†’ Persistent P â†’
-    (P âˆ§ Q -âˆ— atomic_acc Eo Ei Î± Q Î² Î¦) â†’
-    P âˆ§ Q -âˆ— atomic_update Eo Ei Î± Î² Î¦.
+    (P âˆ§ Q âŠ¢ atomic_acc Eo Ei Î± Q Î² Î¦) â†’
+    P âˆ§ Q âŠ¢ atomic_update Eo Ei Î± Î² Î¦.
   Proof.
     rewrite atomic_update_unseal {1}/atomic_update_def /=.
     iIntros (?? HAU) "[#HP HQ]".
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 2beffa800..6b985d9ec 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -41,16 +41,19 @@ Section fractional.
   Lemma fractional_split_1 P P1 P2 Î¦ q1 q2 :
     AsFractional P Î¦ (q1 + q2) â†’ AsFractional P1 Î¦ q1 â†’ AsFractional P2 Î¦ q2 â†’
     P -âˆ— P1 âˆ— P2.
-  Proof. intros. by rewrite -(fractional_split P). Qed.
+  Proof. intros. apply bi.entails_wand. by rewrite -(fractional_split P). Qed.
   Lemma fractional_split_2 P P1 P2 Î¦ q1 q2 :
     AsFractional P Î¦ (q1 + q2) â†’ AsFractional P1 Î¦ q1 â†’ AsFractional P2 Î¦ q2 â†’
     P1 -âˆ— P2 -âˆ— P.
-  Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
+  Proof. intros. apply bi.entails_wand, bi.wand_intro_r. by rewrite -(fractional_split P). Qed.
 
   Lemma fractional_merge P1 P2 Î¦ q1 q2 `{!Fractional Î¦} :
     AsFractional P1 Î¦ q1 â†’ AsFractional P2 Î¦ q2 â†’
     P1 -âˆ— P2 -âˆ— Î¦ (q1 + q2)%Qp.
-  Proof. move=>-[-> _] [-> _]. rewrite fractional. apply bi.wand_intro_r. done. Qed.
+  Proof.
+    move=>-[-> _] [-> _]. rewrite fractional.
+    apply bi.entails_wand, bi.wand_intro_r. done.
+  Qed.
 
   Lemma fractional_half P P12 Î¦ q :
     AsFractional P Î¦ q â†’ AsFractional P12 Î¦ (q/2) â†’
@@ -59,11 +62,11 @@ Section fractional.
   Lemma fractional_half_1 P P12 Î¦ q :
     AsFractional P Î¦ q â†’ AsFractional P12 Î¦ (q/2) â†’
     P -âˆ— P12 âˆ— P12.
-  Proof. intros. by rewrite -(fractional_half P). Qed.
+  Proof. intros. apply bi.entails_wand. by rewrite -(fractional_half P). Qed.
   Lemma fractional_half_2 P P12 Î¦ q :
     AsFractional P Î¦ q â†’ AsFractional P12 Î¦ (q/2) â†’
     P12 -âˆ— P12 -âˆ— P.
-  Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
+  Proof. intros. apply bi.entails_wand, bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
 
   (** Fractional and logical connectives *)
   Global Instance persistent_fractional (P : PROP) :
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 94fd101c5..1a03007f7 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
 
 (** The class of laterable assertions *)
 Class Laterable {PROP : bi} (P : PROP) := laterable :
-  P -âˆ— âˆƒ Q, â–· Q âˆ— â–¡ (â–· Q -âˆ— â—‡ P).
+  P âŠ¢ âˆƒ Q, â–· Q âˆ— â–¡ (â–· Q -âˆ— â—‡ P).
 Global Arguments Laterable {_} _%I : simpl never.
 Global Arguments laterable {_} _%I {_}.
 Global Hint Mode Laterable + ! : typeclass_instances.
@@ -129,14 +129,14 @@ Section instances.
   Proof. by intros ->. Qed.
 
   Lemma make_laterable_except_0 Q :
-    make_laterable (â—‡ Q) -âˆ— make_laterable Q.
+    make_laterable (â—‡ Q) âŠ¢ make_laterable Q.
   Proof.
     iIntros "(%P & HP & #HPQ)". iExists P. iFrame.
     iIntros "!# HP". iMod ("HPQ" with "HP"). done.
   Qed.
 
   Lemma make_laterable_sep Q1 Q2 :
-    make_laterable Q1 âˆ— make_laterable Q2 -âˆ— make_laterable (Q1 âˆ— Q2).
+    make_laterable Q1 âˆ— make_laterable Q2 âŠ¢ make_laterable (Q1 âˆ— Q2).
   Proof.
     iIntros "[HQ1 HQ2]".
     iDestruct "HQ1" as (P1) "[HP1 #HQ1]".
@@ -151,7 +151,7 @@ Section instances.
   resources. We cannot keep arbitrary resources since that would let us "frame
   in" non-laterable things. *)
   Lemma make_laterable_wand Q1 Q2 :
-    make_laterable (Q1 -âˆ— Q2) -âˆ— (make_laterable Q1 -âˆ— make_laterable Q2).
+    make_laterable (Q1 -âˆ— Q2) âŠ¢ (make_laterable Q1 -âˆ— make_laterable Q2).
   Proof.
     iIntros "HQ HQ1".
     iDestruct (make_laterable_sep with "[$HQ $HQ1 //]") as "HQ".
@@ -162,7 +162,7 @@ Section instances.
   (** A variant of the above for keeping arbitrary intuitionistic resources.
       Sadly, this is not implied by the above for non-affine BIs. *)
   Lemma make_laterable_intuitionistic_wand Q1 Q2 :
-    â–¡ (Q1 -âˆ— Q2) -âˆ— (make_laterable Q1 -âˆ— make_laterable Q2).
+    â–¡ (Q1 -âˆ— Q2) âŠ¢ (make_laterable Q1 -âˆ— make_laterable Q2).
   Proof.
     iIntros "#HQ HQ1". iDestruct "HQ1" as (P) "[HP #HQ1]".
     iExists P. iFrame. iIntros "!> HP".
@@ -178,7 +178,7 @@ Section instances.
   Qed.
 
   Lemma make_laterable_elim Q :
-    make_laterable Q -âˆ— â—‡ Q.
+    make_laterable Q âŠ¢ â—‡ Q.
   Proof.
     iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]". by iApply "HQ".
   Qed.
@@ -197,7 +197,7 @@ Section instances.
   Qed.
   Lemma make_laterable_intro' Q :
     Laterable Q â†’
-    Q -âˆ— make_laterable Q.
+    Q âŠ¢ make_laterable Q.
   Proof.
     intros ?. iApply make_laterable_intro. iIntros "!# $".
   Qed.
@@ -213,7 +213,7 @@ Section instances.
   Qed.
 
   Lemma laterable_alt Q :
-    Laterable Q â†” (Q -âˆ— make_laterable Q).
+    Laterable Q â†” (Q âŠ¢ make_laterable Q).
   Proof.
     split.
     - intros ?. apply make_laterable_intro'. done.
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index a60458654..be4223c72 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -321,7 +321,7 @@ Section general.
   Qed.
 
   Lemma bi_nsteps_add_inv n m x z :
-    bi_nsteps R (n + m) x z -âˆ— âˆƒ y, bi_nsteps R n x y âˆ— bi_nsteps R m y z.
+    bi_nsteps R (n + m) x z âŠ¢ âˆƒ y, bi_nsteps R n x y âˆ— bi_nsteps R m y z.
   Proof.
     iInduction n as [|n] "IH" forall (x).
     - iIntros "Hxz". iExists x. auto.
@@ -332,7 +332,7 @@ Section general.
   Qed.
 
   Lemma bi_nsteps_inv_r n x z :
-    bi_nsteps R (S n) x z -âˆ— âˆƒ y, bi_nsteps R n x y âˆ— R y z.
+    bi_nsteps R (S n) x z âŠ¢ âˆƒ y, bi_nsteps R n x y âˆ— R y z.
   Proof.
     rewrite -Nat.add_1_r bi_nsteps_add_inv /=.
     iDestruct 1 as (y) "[Hxy (%x' & Hxx' & Heq)]".
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index f6a80ead4..978c53876 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -656,7 +656,7 @@ Module Import monPred.
 End monPred.
 
 Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
-  objective_at i j : P i -âˆ— P j.
+  objective_at i j : P i âŠ¢ P j.
 Global Arguments Objective {_ _} _%I.
 Global Arguments objective_at {_ _} _%I {_}.
 Global Hint Mode Objective + + ! : typeclass_instances.
@@ -716,9 +716,9 @@ Section bi_facts.
   Lemma monPred_at_absorbingly_if i p P : (<absorb>?p P) i âŠ£âŠ¢ <absorb>?p (P i).
   Proof. destruct p=>//=. apply monPred_at_absorbingly. Qed.
 
-  Lemma monPred_wand_force i P Q : (P -âˆ— Q) i -âˆ— (P i -âˆ— Q i).
+  Lemma monPred_wand_force i P Q : (P -âˆ— Q) i âŠ¢ (P i -âˆ— Q i).
   Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
-  Lemma monPred_impl_force i P Q : (P â†’ Q) i -âˆ— (P i â†’ Q i).
+  Lemma monPred_impl_force i P Q : (P â†’ Q) i âŠ¢ (P i â†’ Q i).
   Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
 
   (** Instances *)
@@ -983,7 +983,7 @@ Section bi_facts.
     unseal. split=>i /=.
     rewrite /= -(bi.exist_intro i). apply bi.and_intro=>//. by apply bi.pure_intro.
   Qed.
-  Lemma monPred_in_elim P i : monPred_in i -âˆ— âŽ¡P iâŽ¤ â†’ P .
+  Lemma monPred_in_elim P i : monPred_in i âŠ¢ âŽ¡P iâŽ¤ â†’ P .
   Proof.
     apply bi.impl_intro_r. unseal. split=>i' /=.
     eapply bi.pure_elim; [apply bi.and_elim_l|]=>?. rewrite bi.and_elim_r. by f_equiv.
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 07aef3987..3f87dbfc3 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -158,7 +158,7 @@ Section plainly_derived.
   Lemma absorbingly_elim_plainly P : <absorb> â–  P âŠ£âŠ¢ â–  P.
   Proof. by rewrite -(persistently_elim_plainly P) absorbingly_elim_persistently. Qed.
 
-  Lemma plainly_and_sep_elim P Q : â–  P âˆ§ Q -âˆ— (emp âˆ§ P) âˆ— Q.
+  Lemma plainly_and_sep_elim P Q : â–  P âˆ§ Q âŠ¢ (emp âˆ§ P) âˆ— Q.
   Proof. by rewrite plainly_elim_persistently persistently_and_sep_elim_emp. Qed.
   Lemma plainly_and_sep_assoc P Q R : â–  P âˆ§ (Q âˆ— R) âŠ£âŠ¢ (â–  P âˆ§ Q) âˆ— R.
   Proof. by rewrite -(persistently_elim_plainly P) persistently_and_sep_assoc. Qed.
@@ -235,9 +235,9 @@ Section plainly_derived.
   Lemma plainly_affinely_elim P : â–  <affine> P âŠ£âŠ¢ â–  P.
   Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
 
-  Lemma intuitionistically_plainly_elim P : â–¡ â–  P -âˆ— â–¡ P.
+  Lemma intuitionistically_plainly_elim P : â–¡ â–  P âŠ¢ â–¡ P.
   Proof. rewrite intuitionistically_affinely plainly_elim_persistently //. Qed.
-  Lemma intuitionistically_plainly P : â–¡ â–  P -âˆ— â–  â–¡ P.
+  Lemma intuitionistically_plainly P : â–¡ â–  P âŠ¢ â–  â–¡ P.
   Proof.
     rewrite /bi_intuitionistically plainly_affinely_elim affinely_elim.
     rewrite persistently_elim_plainly plainly_persistently_elim. done.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index deb35e594..ade5e6377 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -20,8 +20,8 @@ Global Arguments bupd {_}%type_scope {_} _%bi_scope.
 Global Typeclasses Opaque bupd.
 
 Notation "|==> Q" := (bupd Q) : bi_scope.
-Notation "P ==âˆ— Q" := (P âŠ¢ |==> Q) (only parsing) : stdpp_scope.
 Notation "P ==âˆ— Q" := (P -âˆ— |==> Q)%I : bi_scope.
+Notation "P ==âˆ— Q" := (P -âˆ— |==> Q) : stdpp_scope.
 
 Class FUpd (PROP : Type) : Type := fupd : coPset â†’ coPset â†’ PROP â†’ PROP.
 Global Instance: Params (@fupd) 4 := {}.
@@ -45,7 +45,7 @@ Notation "P ={ E }=âˆ— Q" := (P -âˆ— |={E}=> Q) : stdpp_scope.
     than for the two masks of a mask-changing updates. *)
 Notation "|={ Eo } [ Ei ]â–·=> Q" := (|={Eo,Ei}=> â–· |={Ei,Eo}=> Q)%I : bi_scope.
 Notation "P ={ Eo } [ Ei ]â–·=âˆ— Q" := (P -âˆ— |={Eo}[Ei]â–·=> Q)%I : bi_scope.
-Notation "P ={ Eo } [ Ei ]â–·=âˆ— Q" := (P -âˆ— |={Eo}[Ei]â–·=> Q) (only parsing) : stdpp_scope.
+Notation "P ={ Eo } [ Ei ]â–·=âˆ— Q" := (P -âˆ— |={Eo}[Ei]â–·=> Q) : stdpp_scope.
 
 Notation "|={ E }â–·=> Q" := (|={E}[E]â–·=> Q)%I : bi_scope.
 Notation "P ={ E }â–·=âˆ— Q" := (P ={E}[E]â–·=âˆ— Q)%I : bi_scope.
@@ -58,20 +58,20 @@ Notation "P ={ E }â–·=âˆ— Q" := (P ={E}[E]â–·=âˆ— Q) : stdpp_scope.
     |={E1,Eo}=> |={Eo}[Ei]â–·=>^n |={Eo,E2}=> Q] *)
 Notation "|={ Eo } [ Ei ]â–·=>^ n Q" := (Nat.iter n (Î» P, |={Eo}[Ei]â–·=> P) Q)%I : bi_scope.
 Notation "P ={ Eo } [ Ei ]â–·=âˆ—^ n Q" := (P -âˆ— |={Eo}[Ei]â–·=>^n Q)%I : bi_scope.
-Notation "P ={ Eo } [ Ei ]â–·=âˆ—^ n Q" := (P -âˆ— |={Eo}[Ei]â–·=>^n Q) (only parsing) : stdpp_scope.
+Notation "P ={ Eo } [ Ei ]â–·=âˆ—^ n Q" := (P -âˆ— |={Eo}[Ei]â–·=>^n Q) : stdpp_scope.
 
 Notation "|={ E }â–·=>^ n Q" := (|={E}[E]â–·=>^n Q)%I : bi_scope.
 Notation "P ={ E }â–·=âˆ—^ n Q" := (P ={E}[E]â–·=âˆ—^n Q)%I : bi_scope.
-Notation "P ={ E }â–·=âˆ—^ n Q" := (P ={E}[E]â–·=âˆ—^n Q) (only parsing) : stdpp_scope.
+Notation "P ={ E }â–·=âˆ—^ n Q" := (P ={E}[E]â–·=âˆ—^n Q) : stdpp_scope.
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
   bi_bupd_mixin_bupd_ne : NonExpansive (bupd (PROP:=PROP));
-  bi_bupd_mixin_bupd_intro (P : PROP) : P ==âˆ— P;
-  bi_bupd_mixin_bupd_mono (P Q : PROP) : (P âŠ¢ Q) â†’ (|==> P) ==âˆ— Q;
-  bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) ==âˆ— P;
-  bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) âˆ— R ==âˆ— P âˆ— R;
+  bi_bupd_mixin_bupd_intro (P : PROP) : P âŠ¢ |==> P;
+  bi_bupd_mixin_bupd_mono (P Q : PROP) : (P âŠ¢ Q) â†’ (|==> P) âŠ¢ |==> Q;
+  bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) âŠ¢ |==> P;
+  bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) âˆ— R âŠ¢ |==> P âˆ— R;
 }.
 
 Record BiFUpdMixin (PROP : bi) `(FUpd PROP) := {
@@ -80,15 +80,15 @@ Record BiFUpdMixin (PROP : bi) `(FUpd PROP) := {
   bi_fupd_mixin_fupd_mask_subseteq E1 E2 :
     E2 âŠ† E1 â†’ âŠ¢@{PROP} |={E1,E2}=> |={E2,E1}=> emp;
   bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) :
-    â—‡ (|={E1,E2}=> P) ={E1,E2}=âˆ— P;
+    â—‡ (|={E1,E2}=> P) âŠ¢ |={E1,E2}=> P;
   bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) :
     (P âŠ¢ Q) â†’ (|={E1,E2}=> P) âŠ¢ |={E1,E2}=> Q;
   bi_fupd_mixin_fupd_trans E1 E2 E3 (P : PROP) :
     (|={E1,E2}=> |={E2,E3}=> P) âŠ¢ |={E1,E3}=> P;
   bi_fupd_mixin_fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
-    E1 ## Ef â†’ (|={E1,E2}=> âŒœE2 ## EfâŒ â†’ P) ={E1 âˆª Ef,E2 âˆª Ef}=âˆ— P;
+    E1 ## Ef â†’ (|={E1,E2}=> âŒœE2 ## EfâŒ â†’ P) âŠ¢ |={E1 âˆª Ef,E2 âˆª Ef}=> P;
   bi_fupd_mixin_fupd_frame_r E1 E2 (P R : PROP) :
-    (|={E1,E2}=> P) âˆ— R ={E1,E2}=âˆ— P âˆ— R;
+    (|={E1,E2}=> P) âˆ— R âŠ¢ |={E1,E2}=> P âˆ— R;
 }.
 
 Class BiBUpd (PROP : bi) := {
@@ -106,11 +106,11 @@ Global Hint Mode BiFUpd ! : typeclass_instances.
 Global Arguments bi_fupd_fupd : simpl never.
 
 Class BiBUpdFUpd (PROP : bi) `{BiBUpd PROP, BiFUpd PROP} :=
-  bupd_fupd E (P : PROP) : (|==> P) ={E}=âˆ— P.
+  bupd_fupd E (P : PROP) : (|==> P) âŠ¢ |={E}=> P.
 Global Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
 Class BiBUpdPlainly (PROP : bi) `{!BiBUpd PROP, !BiPlainly PROP} :=
-  bupd_plainly (P : PROP) : (|==> â–  P) -âˆ— P.
+  bupd_plainly (P : PROP) : (|==> â–  P) âŠ¢ P.
 Global Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
 
 (** These rules for the interaction between the [â– ] and [|={E1,E2=>] modalities
@@ -144,13 +144,13 @@ Section bupd_laws.
 
   Global Instance bupd_ne : NonExpansive (@bupd PROP _).
   Proof. eapply bi_bupd_mixin_bupd_ne, bi_bupd_mixin. Qed.
-  Lemma bupd_intro P : P ==âˆ— P.
+  Lemma bupd_intro P : P âŠ¢ |==> P.
   Proof. eapply bi_bupd_mixin_bupd_intro, bi_bupd_mixin. Qed.
-  Lemma bupd_mono (P Q : PROP) : (P âŠ¢ Q) â†’ (|==> P) ==âˆ— Q.
+  Lemma bupd_mono (P Q : PROP) : (P âŠ¢ Q) â†’ (|==> P) âŠ¢ |==> Q.
   Proof. eapply bi_bupd_mixin_bupd_mono, bi_bupd_mixin. Qed.
-  Lemma bupd_trans (P : PROP) : (|==> |==> P) ==âˆ— P.
+  Lemma bupd_trans (P : PROP) : (|==> |==> P) âŠ¢ |==> P.
   Proof. eapply bi_bupd_mixin_bupd_trans, bi_bupd_mixin. Qed.
-  Lemma bupd_frame_r (P R : PROP) : (|==> P) âˆ— R ==âˆ— P âˆ— R.
+  Lemma bupd_frame_r (P R : PROP) : (|==> P) âˆ— R âŠ¢ |==> P âˆ— R.
   Proof. eapply bi_bupd_mixin_bupd_frame_r, bi_bupd_mixin. Qed.
 End bupd_laws.
 
@@ -166,16 +166,16 @@ Section fupd_laws.
   specify the mask. *)
   Lemma fupd_mask_subseteq {E1} E2 : E2 âŠ† E1 â†’ âŠ¢@{PROP} |={E1,E2}=> |={E2,E1}=> emp.
   Proof. eapply bi_fupd_mixin_fupd_mask_subseteq, bi_fupd_mixin. Qed.
-  Lemma except_0_fupd E1 E2 (P : PROP) : â—‡ (|={E1,E2}=> P) ={E1,E2}=âˆ— P.
+  Lemma except_0_fupd E1 E2 (P : PROP) : â—‡ (|={E1,E2}=> P) âŠ¢ |={E1,E2}=> P.
   Proof. eapply bi_fupd_mixin_except_0_fupd, bi_fupd_mixin. Qed.
   Lemma fupd_mono E1 E2 (P Q : PROP) : (P âŠ¢ Q) â†’ (|={E1,E2}=> P) âŠ¢ |={E1,E2}=> Q.
   Proof. eapply bi_fupd_mixin_fupd_mono, bi_fupd_mixin. Qed.
   Lemma fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P) âŠ¢ |={E1,E3}=> P.
   Proof. eapply bi_fupd_mixin_fupd_trans, bi_fupd_mixin. Qed.
   Lemma fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
-    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. eapply bi_fupd_mixin_fupd_mask_frame_r', bi_fupd_mixin. Qed.
-  Lemma fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P) âˆ— R ={E1,E2}=âˆ— P âˆ— R.
+  Lemma fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P) âˆ— R âŠ¢ |={E1,E2}=> P âˆ— R.
   Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
 End fupd_laws.
 
@@ -193,13 +193,13 @@ Section bupd_derived.
   Global Instance bupd_flip_mono' : Proper (flip (âŠ¢) ==> flip (âŠ¢)) (bupd (PROP:=PROP)).
   Proof. intros P Q; apply bupd_mono. Qed.
 
-  Lemma bupd_frame_l R Q : (R âˆ— |==> Q) ==âˆ— 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) âˆ— (|==> P) ==âˆ— 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 : (|==> P) âˆ— (P -âˆ— Q) ==âˆ— 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 : (|==> P) âˆ— (|==> Q) ==âˆ— 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_idemp P : (|==> |==> P) âŠ£âŠ¢ |==> P.
   Proof.
@@ -290,9 +290,9 @@ Section fupd_derived.
     rewrite fupd_mask_subseteq; last exact: HE.
     rewrite !fupd_frame_r. rewrite left_id. done.
   Qed.
-  Lemma fupd_intro E P : P ={E}=âˆ— P.
+  Lemma fupd_intro E P : P âŠ¢ |={E}=> P.
   Proof. by rewrite {1}(fupd_mask_intro_subseteq E E P) // fupd_trans. Qed.
-  Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> â—‡ P) ={E1,E2}=âˆ— P.
+  Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> â—‡ P) âŠ¢ |={E1,E2}=> P.
   Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
   Lemma fupd_idemp E P : (|={E}=> |={E}=> P) âŠ£âŠ¢ |={E}=> P.
   Proof.
@@ -307,7 +307,7 @@ Section fupd_derived.
       will be slightly more convenient. *)
   Lemma fupd_mask_weaken {E1} E2 {E3 P} :
     E2 âŠ† E1 â†’
-    ((|={E2,E1}=> emp) ={E2,E3}=âˆ— P) -âˆ— |={E1,E3}=> P.
+    ((|={E2,E1}=> emp) ={E2,E3}=âˆ— P) âŠ¢ |={E1,E3}=> P.
   Proof.
     intros HE.
     apply wand_entails', wand_intro_r.
@@ -319,22 +319,23 @@ Section fupd_derived.
       This lemma is intended to be [iApply]ed. *)
   Lemma fupd_mask_intro E1 E2 P :
     E2 âŠ† E1 â†’
-    ((|={E2,E1}=> emp) -âˆ— P) -âˆ— |={E1,E2}=> P.
+    ((|={E2,E1}=> emp) -âˆ— P) âŠ¢ |={E1,E2}=> P.
   Proof.
     intros. etrans; [|by apply fupd_mask_weaken]. by rewrite -fupd_intro.
   Qed.
 
-  Lemma fupd_mask_intro_discard E1 E2 P `{!Absorbing P} : E2 âŠ† E1 â†’ P ={E1,E2}=âˆ— P.
+  Lemma fupd_mask_intro_discard E1 E2 P `{!Absorbing P} :
+    E2 âŠ† E1 â†’ P âŠ¢ |={E1,E2}=> P.
   Proof.
     intros. etrans; [|by apply fupd_mask_intro].
     apply wand_intro_r. rewrite sep_elim_l. done.
   Qed.
 
-  Lemma fupd_frame_l E1 E2 R Q : (R âˆ— |={E1,E2}=> Q) ={E1,E2}=âˆ— R âˆ— Q.
+  Lemma fupd_frame_l E1 E2 R Q : (R âˆ— |={E1,E2}=> Q) âŠ¢ |={E1,E2}=> R âˆ— Q.
   Proof. rewrite !(comm _ R); 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.
 
   Global Instance fupd_absorbing E1 E2 P :
@@ -342,23 +343,23 @@ Section fupd_derived.
   Proof. rewrite /Absorbing /bi_absorbingly fupd_frame_l =>-> //. Qed.
 
   Lemma fupd_trans_frame E1 E2 E3 P Q :
-    ((Q ={E2,E3}=âˆ— emp) âˆ— |={E1,E2}=> (Q âˆ— P)) ={E1,E3}=âˆ— P.
+    ((Q ={E2,E3}=âˆ— emp) âˆ— |={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_elim E1 E2 E3 P Q :
-    (Q -âˆ— (|={E2,E3}=> P)) â†’ (|={E1,E2}=> Q) -âˆ— (|={E1,E3}=> P).
+    (Q âŠ¢ (|={E2,E3}=> P)) â†’ (|={E1,E2}=> Q) âŠ¢ (|={E1,E3}=> P).
   Proof. intros ->. rewrite 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.
     intros ?. rewrite -fupd_mask_frame_r' //. f_equiv.
     apply impl_intro_l, and_elim_r.
   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.
@@ -366,7 +367,7 @@ Section fupd_derived.
       an arbitrary mask. *)
   Lemma fupd_mask_frame E E' E1 E2 P :
     E1 âŠ† E â†’
-    (|={E1,E2}=> |={E2 âˆª (E âˆ– E1),E'}=> P) -âˆ— (|={E,E'}=> P).
+    (|={E1,E2}=> |={E2 âˆª (E âˆ– E1),E'}=> P) âŠ¢ (|={E,E'}=> P).
   Proof.
     intros ?. rewrite (fupd_mask_frame_r _ _ (E âˆ– E1)); last set_solver.
     rewrite fupd_trans.
@@ -382,11 +383,11 @@ Section fupd_derived.
     (Q -âˆ— |={Eâˆ–E2,E'}=> (âˆ€ R, (|={E1âˆ–E2,E1}=> R) -âˆ— |={Eâˆ–E2,E}=> R) -âˆ—  P) -âˆ—
     (|={E,E'}=> P).
   Proof.
-    intros HE. apply wand_intro_r. rewrite fupd_frame_r.
+    intros HE. apply entails_wand, wand_intro_r. rewrite fupd_frame_r.
     rewrite wand_elim_r. clear Q.
     rewrite -(fupd_mask_frame E E'); first apply fupd_mono; last done.
     (* The most horrible way to apply fupd_intro_mask *)
-    rewrite -[X in (X -âˆ— _)](right_id emp%I).
+    rewrite -[X in (X âŠ¢ _)](right_id emp%I).
     rewrite (fupd_mask_intro_subseteq (E1 âˆ– E2 âˆª E âˆ– E1) (E âˆ– E2) emp); last first.
     { rewrite {1}(union_difference_L _ _ HE). set_solver. }
     rewrite fupd_frame_l fupd_frame_r. apply fupd_elim.
@@ -428,7 +429,7 @@ Section fupd_derived.
   Lemma fupd_forall E1 E2 A (Î¦ : A â†’ PROP) : (|={E1, E2}=> âˆ€ x : A, Î¦ x) âŠ¢ âˆ€ x : A, |={E1, E2}=> Î¦ x.
   Proof. apply forall_intro=> a. by rewrite -(forall_elim a). 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.
 
   Global Instance fupd_sep_homomorphism E :
@@ -436,20 +437,20 @@ Section fupd_derived.
   Proof. split; [split|]; try apply _; [apply fupd_sep | apply fupd_intro]. Qed.
 
   Lemma big_sepL_fupd {A} E (Î¦ : nat â†’ A â†’ PROP) l :
-    ([âˆ— list] kâ†¦x âˆˆ l, |={E}=> Î¦ k x) ={E}=âˆ— [âˆ— list] kâ†¦x âˆˆ l, Î¦ k x.
+    ([âˆ— list] kâ†¦x âˆˆ l, |={E}=> Î¦ k x) âŠ¢ |={E}=> [âˆ— list] kâ†¦x âˆˆ l, Î¦ k x.
   Proof. by rewrite (big_opL_commute _). Qed.
   Lemma big_sepL2_fupd {A B} E (Î¦ : nat â†’ A â†’ B â†’ PROP) l1 l2 :
-    ([âˆ— list] kâ†¦x;y âˆˆ l1;l2, |={E}=> Î¦ k x y) ={E}=âˆ— [âˆ— list] kâ†¦x;y âˆˆ l1;l2, Î¦ k x y.
+    ([âˆ— list] kâ†¦x;y âˆˆ l1;l2, |={E}=> Î¦ k x y) âŠ¢ |={E}=> [âˆ— list] kâ†¦x;y âˆˆ l1;l2, Î¦ k x y.
   Proof.
     rewrite !big_sepL2_alt !persistent_and_affinely_sep_l.
     etrans; [| by apply fupd_frame_l]. apply sep_mono_r. apply big_sepL_fupd.
   Qed.
 
   Lemma big_sepM_fupd `{Countable K} {A} E (Î¦ : K â†’ A â†’ PROP) m :
-    ([âˆ— 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. by rewrite (big_opM_commute _). Qed.
   Lemma big_sepS_fupd `{Countable A} E (Î¦ : A â†’ PROP) X :
-    ([âˆ— set] x âˆˆ X, |={E}=> Î¦ x) ={E}=âˆ— [âˆ— set] x âˆˆ X, Î¦ x.
+    ([âˆ— set] x âˆˆ X, |={E}=> Î¦ x) âŠ¢ |={E}=> [âˆ— set] x âˆˆ X, Î¦ x.
   Proof. by rewrite (big_opS_commute _). Qed.
   Lemma big_sepMS_fupd `{Countable A} E (Î¦ : A â†’ PROP) l :
     ([âˆ— mset] x âˆˆ l, |={E}=> Î¦ x) âŠ¢ |={E}=> [âˆ— mset] x âˆˆ l, Î¦ x.
@@ -458,7 +459,7 @@ Section fupd_derived.
   (** Fancy updates that take a step derived rules. *)
   Lemma step_fupd_wand Eo Ei P Q : (|={Eo}[Ei]â–·=> P) -âˆ— (P -âˆ— Q) -âˆ— |={Eo}[Ei]â–·=> Q.
   Proof.
-    apply wand_intro_l.
+    apply entails_wand, wand_intro_l.
     by rewrite (later_intro (P -âˆ— Q)) fupd_frame_l -later_sep fupd_frame_l
                wand_elim_l.
   Qed.
@@ -484,11 +485,11 @@ Section fupd_derived.
     by rewrite fupd_frame_r left_id.
   Qed.
 
-  Lemma step_fupd_intro Ei Eo P : Ei âŠ† Eo â†’ â–· P -âˆ— |={Eo}[Ei]â–·=> P.
+  Lemma step_fupd_intro Ei Eo P : Ei âŠ† Eo â†’ â–· P âŠ¢ |={Eo}[Ei]â–·=> P.
   Proof. intros. by rewrite -(step_fupd_mask_mono Ei _ Ei _) // -!fupd_intro. Qed.
 
   Lemma step_fupd_frame_l Eo Ei R Q :
-    (R âˆ— |={Eo}[Ei]â–·=> Q) -âˆ— |={Eo}[Ei]â–·=> (R âˆ— Q).
+    (R âˆ— |={Eo}[Ei]â–·=> Q) âŠ¢ |={Eo}[Ei]â–·=> (R âˆ— Q).
   Proof.
     rewrite fupd_frame_l.
     apply fupd_mono.
@@ -512,13 +513,13 @@ Section fupd_derived.
   Lemma step_fupdN_wand Eo Ei n P Q :
     (|={Eo}[Ei]â–·=>^n P) -âˆ— (P -âˆ— Q) -âˆ— (|={Eo}[Ei]â–·=>^n Q).
   Proof.
-    apply wand_intro_l. induction n as [|n IH]=> /=.
+    apply entails_wand, wand_intro_l. induction n as [|n IH]=> /=.
     { by rewrite wand_elim_l. }
     rewrite -IH -fupd_frame_l later_sep -fupd_frame_l.
     by apply sep_mono; first apply later_intro.
   Qed.
 
-  Lemma step_fupdN_intro Ei Eo n P : Ei âŠ† Eo â†’ â–·^n P -âˆ— |={Eo}[Ei]â–·=>^n P.
+  Lemma step_fupdN_intro Ei Eo n P : Ei âŠ† Eo â†’ â–·^n P âŠ¢ |={Eo}[Ei]â–·=>^n P.
   Proof.
     induction n as [|n IH]=> ?; [done|].
     rewrite /= -step_fupd_intro; [|done]. by rewrite IH.
@@ -532,7 +533,7 @@ Section fupd_derived.
   Qed.
 
   Lemma step_fupdN_frame_l Eo Ei n R Q :
-    (R âˆ— |={Eo}[Ei]â–·=>^n Q) -âˆ— |={Eo}[Ei]â–·=>^n (R âˆ— Q).
+    (R âˆ— |={Eo}[Ei]â–·=>^n Q) âŠ¢ |={Eo}[Ei]â–·=>^n (R âˆ— Q).
   Proof.
     induction n as [|n IH]; simpl; [done|].
     rewrite step_fupd_frame_l IH //=.
@@ -548,7 +549,7 @@ Section fupd_derived.
     this lemma introduces updates in the same way as [step_fupdN_intro]
     (in fact, for [n = 0] it is essentially [step_fupdN_intro], modulo laters). *)
   Lemma step_fupdN_le n m Eo Ei P :
-    n â‰¤ m â†’ Ei âŠ† Eo â†’ (|={Eo}[Ei]â–·=>^n P) -âˆ— (|={Eo}[Ei]â–·=>^m P).
+    n â‰¤ m â†’ Ei âŠ† Eo â†’ (|={Eo}[Ei]â–·=>^n P) âŠ¢ (|={Eo}[Ei]â–·=>^m P).
   Proof.
     intros ??. replace m with ((m - n) + n) by lia.
     rewrite step_fupdN_add.
@@ -565,7 +566,7 @@ Section fupd_derived.
       apply fupd_elim, (fupd_mask_intro_discard _ _ _). set_solver.
     Qed.
 
-    Lemma fupd_plainly_elim E P : â–  P ={E}=âˆ— P.
+    Lemma fupd_plainly_elim E P : â–  P âŠ¢ |={E}=> P.
     Proof. by rewrite (fupd_intro E (â–  P)) fupd_plainly_mask. Qed.
 
     Lemma fupd_plainly_keep_r E P R : R âˆ— (R ={E}=âˆ— â–  P) âŠ¢ |={E}=> R âˆ— P.
@@ -615,13 +616,13 @@ Section fupd_derived.
       (|={E}=> âˆ€ x, Î¦ x) âŠ£âŠ¢ (âˆ€ x, |={E}=> Î¦ x).
     Proof. by apply fupd_plain_forall. Qed.
 
-    Lemma step_fupd_plain Eo Ei P `{!Plain P} : (|={Eo}[Ei]â–·=> P) ={Eo}=âˆ— â–· â—‡ P.
+    Lemma step_fupd_plain Eo Ei P `{!Plain P} : (|={Eo}[Ei]â–·=> P) âŠ¢ |={Eo}=> â–· â—‡ P.
     Proof.
       rewrite -(fupd_plain_mask _ Ei (â–· â—‡ P)).
       apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
     Qed.
 
-    Lemma step_fupdN_plain Eo Ei n P `{!Plain P} : (|={Eo}[Ei]â–·=>^n P) ={Eo}=âˆ— â–·^n â—‡ P.
+    Lemma step_fupdN_plain Eo Ei n P `{!Plain P} : (|={Eo}[Ei]â–·=>^n P) âŠ¢ |={Eo}=> â–·^n â—‡ P.
     Proof.
       induction n as [|n IH].
       - by rewrite -fupd_intro -except_0_intro.
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index 522fab8b6..c5078fd67 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -177,7 +177,7 @@ Lemma wp_pure_step_later `{!Inhabited (state Î›)} s E e1 e2 Ï† n Î¦ :
   â–·^n (Â£ n -âˆ— WP e2 @ s; E {{ Î¦ }}) âŠ¢ WP e1 @ s; E {{ Î¦ }}.
 Proof.
   intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec.
-  enough (âˆ€ P, â–·^n P -âˆ— |={E}â–·=>^n P) as Hwp by apply Hwp. iIntros (?).
+  enough (âˆ€ P, â–·^n P âŠ¢ |={E}â–·=>^n P) as Hwp by apply Hwp. iIntros (?).
   induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH.
 Qed.
 End lifting.
diff --git a/iris/program_logic/ownp.v b/iris/program_logic/ownp.v
index 842e8520a..64597474c 100644
--- a/iris/program_logic/ownp.v
+++ b/iris/program_logic/ownp.v
@@ -197,7 +197,7 @@ Section lifting.
     {{{ â–· (ownP Ïƒ1) }}} e1 @ s; E {{{ RET v2; ownP Ïƒ2 }}}.
   Proof.
     intros. rewrite -(ownP_lift_atomic_det_step Ïƒ1 v2 Ïƒ2 []); [|done..].
-    rewrite big_sepL_nil right_id. apply bi.wand_intro_r. iIntros "[Hs Hs']".
+    rewrite big_sepL_nil right_id. iIntros "Hs Hs'".
     iSplitL "Hs"; first by iFrame. iModIntro. iIntros "HÏƒ2". iApply "Hs'". iFrame.
   Qed.
 
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 992fb12cb..b53b66523 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -127,17 +127,17 @@ Proof.
     iApply "IH"; auto.
 Qed.
 
-Lemma fupd_twp s E e Î¦ : (|={E}=> WP e @ s; E [{ Î¦ }]) -âˆ— WP e @ s; E [{ Î¦ }].
+Lemma fupd_twp s E e Î¦ : (|={E}=> WP e @ s; E [{ Î¦ }]) âŠ¢ WP e @ s; E [{ Î¦ }].
 Proof.
   rewrite twp_unfold /twp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
   iIntros (Ïƒ1 ns Îºs nt) "HÏƒ1". iMod "H". by iApply "H".
 Qed.
-Lemma twp_fupd s E e Î¦ : WP e @ s; E [{ v, |={E}=> Î¦ v }] -âˆ— WP e @ s; E [{ Î¦ }].
+Lemma twp_fupd s E e Î¦ : WP e @ s; E [{ v, |={E}=> Î¦ v }] âŠ¢ WP e @ s; E [{ Î¦ }].
 Proof. iIntros "H". iApply (twp_strong_mono with "H"); auto. Qed.
 
 Lemma twp_atomic s E1 E2 e Î¦ `{!Atomic (stuckness_to_atomicity s) e} :
-  (|={E1,E2}=> WP e @ s; E2 [{ v, |={E2,E1}=> Î¦ v }]) -âˆ— WP e @ s; E1 [{ Î¦ }].
+  (|={E1,E2}=> WP e @ s; E2 [{ v, |={E2,E1}=> Î¦ v }]) âŠ¢ WP e @ s; E1 [{ Î¦ }].
 Proof.
   iIntros "H". rewrite !twp_unfold /twp_pre /=.
   destruct (to_val e) as [v|] eqn:He.
@@ -155,7 +155,7 @@ Proof.
 Qed.
 
 Lemma twp_bind K `{!LanguageCtx K} s E e Î¦ :
-  WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Î¦ }] }] -âˆ— WP K e @ s; E [{ Î¦ }].
+  WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Î¦ }] }] âŠ¢ WP K e @ s; E [{ Î¦ }].
 Proof.
   revert Î¦. cut (âˆ€ Î¦', WP e @ s; E [{ Î¦' }] -âˆ— âˆ€ Î¦,
     (âˆ€ v, Î¦' v -âˆ— WP K (of_val v) @ s; E [{ Î¦ }]) -âˆ— WP K e @ s; E [{ Î¦ }]).
@@ -215,7 +215,7 @@ Qed.
 
 (** * Derived rules *)
 Lemma twp_mono s E e Î¦ Î¨ :
-  (âˆ€ v, Î¦ v -âˆ— Î¨ v) â†’ WP e @ s; E [{ Î¦ }] -âˆ— WP e @ s; E [{ Î¨ }].
+  (âˆ€ v, Î¦ v âŠ¢ Î¨ v) â†’ WP e @ s; E [{ Î¦ }] âŠ¢ WP e @ s; E [{ Î¨ }].
 Proof.
   iIntros (HÎ¦) "H"; iApply (twp_strong_mono with "H"); auto.
   iIntros (v) "?". by iApply HÎ¦.
@@ -240,9 +240,9 @@ Proof. rewrite twp_value_fupd'. auto. Qed.
 Lemma twp_value s E Î¦ e v : IntoVal e v â†’ Î¦ v âŠ¢ WP e @ s; E [{ Î¦ }].
 Proof. intros <-. apply twp_value'. Qed.
 
-Lemma twp_frame_l s E e Î¦ R : R âˆ— WP e @ s; E [{ Î¦ }] -âˆ— WP e @ s; E [{ v, R âˆ— Î¦ v }].
+Lemma twp_frame_l s E e Î¦ R : R âˆ— WP e @ s; E [{ Î¦ }] âŠ¢ WP e @ s; E [{ v, R âˆ— Î¦ v }].
 Proof. iIntros "[? H]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.
-Lemma twp_frame_r s E e Î¦ R : WP e @ s; E [{ Î¦ }] âˆ— R -âˆ— WP e @ s; E [{ v, Î¦ v âˆ— R }].
+Lemma twp_frame_r s E e Î¦ R : WP e @ s; E [{ Î¦ }] âˆ— R âŠ¢ WP e @ s; E [{ v, Î¦ v âˆ— R }].
 Proof. iIntros "[H ?]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.
 
 Lemma twp_wand s E e Î¦ Î¨ :
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 07bbb2da3..20307af26 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -43,7 +43,7 @@ Class irisGS_gen (hlc : has_lc) (Î› : language) (Î£ : gFunctors) := IrisG {
   complicate the formalization in Iris, we prefer simplifying the
   client. *)
   state_interp_mono Ïƒ ns Îºs nt:
-    state_interp Ïƒ ns Îºs nt ={âˆ…}=âˆ— state_interp Ïƒ (S ns) Îºs nt
+    state_interp Ïƒ ns Îºs nt âŠ¢ |={âˆ…}=> state_interp Ïƒ (S ns) Îºs nt
 }.
 Global Opaque iris_invGS.
 Global Arguments IrisG {hlc Î› Î£}.
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 24ecc9a6a..8f61cdb17 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -23,7 +23,7 @@ Global Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
     Used when framing encounters a monPred_at in the goal. *)
 Class FrameMonPredAt {I : biIndex} {PROP : bi} (p : bool) (i : I)
       (ð“¡ : PROP) (P : monPred I PROP) (ð“  : PROP) :=
-  frame_monPred_at : â–¡?p ð“¡ âˆ— ð“  -âˆ— P i.
+  frame_monPred_at : â–¡?p ð“¡ âˆ— ð“  âŠ¢ P i.
 Global Arguments FrameMonPredAt {_ _} _ _ _%I _%I _%I.
 Global Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.
 
@@ -391,7 +391,7 @@ Global Instance frame_monPred_at_wand p P R Q1 Q2 i j :
 Proof.
   rewrite /IsBiIndexRel /Frame /FrameMonPredAt=>-> Hframe.
   rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
-  change ((â–¡?p R âˆ— (P -âˆ— Q2)) -âˆ— P -âˆ— Q1). apply bi.wand_intro_r.
+  change ((â–¡?p R âˆ— (P -âˆ— Q2)) âŠ¢ P -âˆ— Q1). apply bi.wand_intro_r.
   rewrite -assoc bi.wand_elim_l. done.
 Qed.
 Global Instance frame_monPred_at_impl P R Q1 Q2 i j :
@@ -401,7 +401,7 @@ Global Instance frame_monPred_at_impl P R Q1 Q2 i j :
 Proof.
   rewrite /IsBiIndexRel /Frame /FrameMonPredAt=>-> Hframe.
   rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
-  change ((â–¡ R âˆ— (P â†’ Q2)) -âˆ— P â†’ Q1).
+  change ((â–¡ R âˆ— (P â†’ Q2)) âŠ¢ P â†’ Q1).
   rewrite -bi.persistently_and_intuitionistically_sep_l. apply bi.impl_intro_r.
   rewrite -assoc bi.impl_elim_l bi.persistently_and_intuitionistically_sep_l. done.
 Qed.
diff --git a/iris_deprecated/base_logic/sts.v b/iris_deprecated/base_logic/sts.v
index 642fc5ab7..b20282c00 100644
--- a/iris_deprecated/base_logic/sts.v
+++ b/iris_deprecated/base_logic/sts.v
@@ -75,25 +75,25 @@ Section sts.
   Lemma sts_ownS_weaken Î³ S1 S2 T1 T2 :
     T2 âŠ† T1 â†’ S1 âŠ† S2 â†’ sts.closed S2 T2 â†’
     sts_ownS Î³ S1 T1 ==âˆ— sts_ownS Î³ S2 T2.
-  Proof. intros ???. by apply own_update, sts_update_frag. Qed.
+  Proof. intros ???. iApply own_update. by apply sts_update_frag. Qed.
 
   Lemma sts_own_weaken Î³ s S T1 T2 :
     T2 âŠ† T1 â†’ s âˆˆ S â†’ sts.closed S T2 â†’
     sts_own Î³ s T1 ==âˆ— sts_ownS Î³ S T2.
-  Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
+  Proof. intros ???. iApply own_update. by apply sts_update_frag_up. Qed.
 
   Lemma sts_own_weaken_state Î³ s1 s2 T :
     sts.frame_steps T s2 s1 â†’ sts.tok s2 ## T â†’
     sts_own Î³ s1 T ==âˆ— sts_own Î³ s2 T.
   Proof.
-    intros ??. apply own_update, sts_update_frag_up; [|done..].
+    intros ??. iApply own_update. apply sts_update_frag_up; [|done..].
     intros Hdisj. apply sts.closed_up. done.
   Qed.
 
   Lemma sts_own_weaken_tok Î³ s T1 T2 :
     T2 âŠ† T1 â†’ sts_own Î³ s T1 ==âˆ— sts_own Î³ s T2.
   Proof.
-    intros ?. apply own_update, sts_update_frag_up; last done.
+    intros ?. iApply own_update. apply sts_update_frag_up; last done.
     - intros. apply sts.closed_up. set_solver.
     - apply sts.elem_of_up.
   Qed.
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 050b62ce6..85b326faa 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -56,7 +56,7 @@ Section steps.
 
   Lemma steps_lb_le n n' :
     n' â‰¤ n â†’ steps_lb n -âˆ— steps_lb n'.
-  Proof. intros Hle. by apply mono_nat_lb_own_le. Qed.
+  Proof. intros Hle. by iApply mono_nat_lb_own_le. Qed.
 
 End steps.
 
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 3c2dd0c0e..7c048fcf5 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -276,7 +276,7 @@ Lemma tac_wp_allocN Î” Î”' s E j K v n Î¦ :
   envs_entails Î” (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E {{ Î¦ }}).
 Proof.
   rewrite envs_entails_unseal=> ? ? HÎ”.
-  rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN.
+  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_allocN.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   specialize (HÎ” l).
   destruct (envs_app _ _ _) as [Î”''|] eqn:HÎ”'; [ | contradiction ].
@@ -294,7 +294,7 @@ Lemma tac_twp_allocN Î” s E j K v n Î¦ :
   envs_entails Î” (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E [{ Î¦ }]).
 Proof.
   rewrite envs_entails_unseal=> ? HÎ”.
-  rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN.
+  rewrite -twp_bind. eapply wand_apply; first by apply wand_entails, twp_allocN.
   rewrite left_id. apply forall_intro=> l.
   specialize (HÎ” l).
   destruct (envs_app _ _ _) as [Î”'|] eqn:HÎ”'; [ | contradiction ].
@@ -313,7 +313,7 @@ Lemma tac_wp_alloc Î” Î”' s E j K v Î¦ :
   envs_entails Î” (WP fill K (Alloc (Val v)) @ s; E {{ Î¦ }}).
 Proof.
   rewrite envs_entails_unseal=> ? HÎ”.
-  rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
+  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_alloc.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   specialize (HÎ” l).
   destruct (envs_app _ _ _) as [Î”''|] eqn:HÎ”'; [ | contradiction ].
@@ -330,7 +330,7 @@ Lemma tac_twp_alloc Î” s E j K v Î¦ :
   envs_entails Î” (WP fill K (Alloc (Val v)) @ s; E [{ Î¦ }]).
 Proof.
   rewrite envs_entails_unseal=> HÎ”.
-  rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
+  rewrite -twp_bind. eapply wand_apply; first by apply wand_entails, twp_alloc.
   rewrite left_id. apply forall_intro=> l.
   specialize (HÎ” l).
   destruct (envs_app _ _ _) as [Î”''|] eqn:HÎ”'; [ | contradiction ].
@@ -346,7 +346,7 @@ Lemma tac_wp_free Î” Î”' s E i K l v Î¦ :
   envs_entails Î” (WP fill K (Free (LitV l)) @ s; E {{ Î¦ }}).
 Proof.
   rewrite envs_entails_unseal=> ? Hlk Hfin.
-  rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
+  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_free.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
   apply later_mono, sep_mono_r, wand_intro_r. rewrite right_id //.
@@ -358,7 +358,7 @@ Lemma tac_twp_free Î” s E i K l v Î¦ :
   envs_entails Î” (WP fill K (Free (LitV l)) @ s; E [{ Î¦ }]).
 Proof.
   rewrite envs_entails_unseal=> Hlk Hfin.
-  rewrite -twp_bind. eapply wand_apply; first exact: twp_free.
+  rewrite -twp_bind. eapply wand_apply; first by apply wand_entails, twp_free.
   rewrite envs_lookup_split //; simpl.
   rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
   apply sep_mono_r, wand_intro_r. rewrite right_id //.
@@ -371,7 +371,7 @@ Lemma tac_wp_load Î” Î”' s E i K b l q v Î¦ :
   envs_entails Î” (WP fill K (Load (LitV l)) @ s; E {{ Î¦ }}).
 Proof.
   rewrite envs_entails_unseal=> ?? Hi.
-  rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
+  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   apply later_mono.
   destruct b; simpl.
@@ -384,7 +384,7 @@ Lemma tac_twp_load Î” s E i K b l q v Î¦ :
   envs_entails Î” (WP fill K (Load (LitV l)) @ s; E [{ Î¦ }]).
 Proof.
   rewrite envs_entails_unseal=> ? Hi.
-  rewrite -twp_bind. eapply wand_apply; first exact: twp_load.
+  rewrite -twp_bind. eapply wand_apply; first by apply wand_entails, twp_load.
   rewrite envs_lookup_split //; simpl.
   destruct b; simpl.
   - iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#".
@@ -402,7 +402,7 @@ Lemma tac_wp_store Î” Î”' s E i K l v v' Î¦ :
 Proof.
   rewrite envs_entails_unseal=> ???.
   destruct (envs_simple_replace _ _ _) as [Î”''|] eqn:HÎ”''; [ | contradiction ].
-  rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
+  rewrite -wp_bind. eapply wand_apply; first by eapply wand_entails, wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -416,7 +416,7 @@ Lemma tac_twp_store Î” s E i K l v v' Î¦ :
 Proof.
   rewrite envs_entails_unseal. intros.
   destruct (envs_simple_replace _ _ _) as [Î”''|] eqn:HÎ”''; [ | contradiction ].
-  rewrite -twp_bind. eapply wand_apply; first by eapply twp_store.
+  rewrite -twp_bind. eapply wand_apply; first by eapply wand_entails, twp_store.
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
@@ -432,7 +432,7 @@ Lemma tac_wp_xchg Î” Î”' s E i K l v v' Î¦ :
 Proof.
   rewrite envs_entails_unseal=> ???.
   destruct (envs_simple_replace _ _ _) as [Î”''|] eqn:HÎ”''; [ | contradiction ].
-  rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg.
+  rewrite -wp_bind. eapply wand_apply; first by eapply wand_entails, wp_xchg.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id.
   by apply later_mono, sep_mono_r, wand_mono.
@@ -447,7 +447,7 @@ Lemma tac_twp_xchg Î” s E i K l v v' Î¦ :
 Proof.
   rewrite envs_entails_unseal. intros.
   destruct (envs_simple_replace _ _ _) as [Î”''|] eqn:HÎ”''; [ | contradiction ].
-  rewrite -twp_bind. eapply wand_apply; first by eapply twp_xchg.
+  rewrite -twp_bind. eapply wand_apply; first by eapply wand_entails, twp_xchg.
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
@@ -470,11 +470,11 @@ Proof.
   destruct (envs_simple_replace _ _ _ _) as [Î”''|] eqn:HÎ”''; [ | contradiction ].
   destruct (decide (v = v1)) as [Heq|Hne].
   - rewrite -wp_bind. eapply wand_apply.
-    { eapply wp_cmpxchg_suc; eauto. }
+    { eapply wand_entails, wp_cmpxchg_suc; eauto. }
     rewrite into_laterN_env_sound -later_sep /= {1}envs_simple_replace_sound //; simpl.
     apply later_mono, sep_mono_r. rewrite right_id. apply wand_mono; auto.
   - rewrite -wp_bind. eapply wand_apply.
-    { eapply wp_cmpxchg_fail; eauto. }
+    { eapply wand_entails, wp_cmpxchg_fail; eauto. }
     rewrite into_laterN_env_sound -later_sep /= {1}envs_lookup_split //; simpl.
     apply later_mono, sep_mono_r. apply wand_mono; auto.
 Qed.
@@ -495,11 +495,11 @@ Proof.
   destruct (envs_simple_replace _ _ _ _) as [Î”''|] eqn:HÎ”''; [ | contradiction ].
   destruct (decide (v = v1)) as [Heq|Hne].
   - rewrite -twp_bind. eapply wand_apply.
-    { eapply twp_cmpxchg_suc; eauto. }
+    { eapply wand_entails, twp_cmpxchg_suc; eauto. }
     rewrite /= {1}envs_simple_replace_sound //; simpl.
     apply sep_mono_r. rewrite right_id. apply wand_mono; auto.
   - rewrite -twp_bind. eapply wand_apply.
-    { eapply twp_cmpxchg_fail; eauto. }
+    { eapply wand_entails, twp_cmpxchg_fail; eauto. }
     rewrite /= {1}envs_lookup_split //; simpl.
     apply sep_mono_r. apply wand_mono; auto.
 Qed.
@@ -512,7 +512,7 @@ Lemma tac_wp_cmpxchg_fail Î” Î”' s E i K l q v v1 v2 Î¦ :
   envs_entails Î” (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Î¦ }}).
 Proof.
   rewrite envs_entails_unseal=> ?????.
-  rewrite -wp_bind. eapply wand_apply; first exact: wp_cmpxchg_fail.
+  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_cmpxchg_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -523,7 +523,7 @@ Lemma tac_twp_cmpxchg_fail Î” s E i K l q v v1 v2 Î¦ :
   envs_entails Î” (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Î¦ }]).
 Proof.
   rewrite envs_entails_unseal. intros. rewrite -twp_bind.
-  eapply wand_apply; first exact: twp_cmpxchg_fail.
+  eapply wand_apply; first by apply wand_entails, twp_cmpxchg_fail.
   (* [//] solves some evars and enables further simplification. *)
   rewrite envs_lookup_split /= // /=. by do 2 f_equiv.
 Qed.
@@ -542,7 +542,7 @@ Proof.
   rewrite envs_entails_unseal=> ?????; subst.
   destruct (envs_simple_replace _ _ _) as [Î”''|] eqn:HÎ”''; [ | contradiction ].
   rewrite -wp_bind. eapply wand_apply.
-  { eapply wp_cmpxchg_suc; eauto. }
+  { eapply wand_entails, wp_cmpxchg_suc; eauto. }
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -559,7 +559,7 @@ Proof.
   rewrite envs_entails_unseal=>????; subst.
   destruct (envs_simple_replace _ _ _) as [Î”''|] eqn:HÎ”''; [ | contradiction ].
   rewrite -twp_bind. eapply wand_apply.
-  { eapply twp_cmpxchg_suc; eauto. }
+  { eapply wand_entails, twp_cmpxchg_suc; eauto. }
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
@@ -575,7 +575,7 @@ Lemma tac_wp_faa Î” Î”' s E i K l z1 z2 Î¦ :
 Proof.
   rewrite envs_entails_unseal=> ???.
   destruct (envs_simple_replace _ _ _) as [Î”''|] eqn:HÎ”''; [ | contradiction ].
-  rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ z1 z2).
+  rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, (wp_faa _ _ _ z1 z2).
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -589,7 +589,7 @@ Lemma tac_twp_faa Î” s E i K l z1 z2 Î¦ :
 Proof.
   rewrite envs_entails_unseal=> ??.
   destruct (envs_simple_replace _ _ _) as [Î”'|] eqn:HÎ”'; [ | contradiction ].
-  rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ z1 z2).
+  rewrite -twp_bind. eapply wand_apply; first by apply wand_entails, (twp_faa _ _ _ z1 z2).
   rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply sep_mono_r, wand_mono.
 Qed.
diff --git a/iris_unstable/base_logic/mono_list.v b/iris_unstable/base_logic/mono_list.v
index 9464fa655..e5422581a 100644
--- a/iris_unstable/base_logic/mono_list.v
+++ b/iris_unstable/base_logic/mono_list.v
@@ -134,11 +134,11 @@ Section mono_list_own.
   Qed.
 
   Lemma mono_list_lb_own_get Î³ q l :
-    mono_list_auth_own Î³ q l -âˆ— mono_list_lb_own Î³ l.
+    mono_list_auth_own Î³ q l âŠ¢ mono_list_lb_own Î³ l.
   Proof. intros. unseal. by apply own_mono, mono_list_included. Qed.
   Lemma mono_list_lb_own_le {Î³ l} l' :
     l' `prefix_of` l â†’
-    mono_list_lb_own Î³ l -âˆ— mono_list_lb_own Î³ l'.
+    mono_list_lb_own Î³ l âŠ¢ mono_list_lb_own Î³ l'.
   Proof. unseal. intros. by apply own_mono, mono_list_lb_mono. Qed.
 
   Lemma mono_list_idx_own_get {Î³ l} i a :
diff --git a/tests/bi_ascii_parsing.ref b/tests/bi_ascii_parsing.ref
index 7fcaf0e59..132bdb884 100644
--- a/tests/bi_ascii_parsing.ref
+++ b/tests/bi_ascii_parsing.ref
@@ -5,4 +5,4 @@ True%I
 "test2"
      : string
 False%I True%I
-(False -âˆ— True)
+(False âŠ¢ True)
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 6626c8ee2..f638ae533 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -38,7 +38,7 @@
   PROP : bi
   Q : PROP
   ============================
-  â–¡ emp âˆ— Q -âˆ— Q
+  â–¡ emp âˆ— Q âŠ¢ Q
 "test_iDestruct_and_emp"
      : string
 1 goal
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 11b3aa042..c1c256a2d 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -107,21 +107,6 @@
      : string
 1 goal
   
-  hlc : has_lc
-  Î£ : gFunctors
-  invGS_gen0 : invGS_gen hlc Î£
-  cinvG0 : cinvG Î£
-  na_invG0 : na_invG Î£
-  t : na_inv_pool_name
-  N : namespace
-  E1, E2 : coPset
-  P : iProp Î£
-  ============================
-  â†‘N âŠ† E2
-  â†’ na_inv t N (<pers> P) âˆ— na_own t E1 âˆ— na_own t E2 ={âŠ¤}=âˆ—
-    na_own t E1 âˆ— na_own t E2 âˆ— â–· P
-1 goal
-  
   hlc : has_lc
   Î£ : gFunctors
   invGS_gen0 : invGS_gen hlc Î£
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index d1b711e53..826831f12 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -126,7 +126,7 @@ Section iris_tests.
   Lemma test_iInv_4 t N E1 E2 P:
     â†‘N âŠ† E2 â†’
     na_inv t N (<pers> P) âˆ— na_own t E1 âˆ— na_own t E2
-         âŠ¢ |={âŠ¤}=> na_own t E1 âˆ— na_own t E2  âˆ— â–· P.
+       ={âŠ¤}=âˆ— na_own t E1 âˆ— na_own t E2  âˆ— â–· P.
   Proof.
     iIntros (?) "(#?&Hown1&Hown2)".
     iInv N as "(#HP&Hown2)". Show.
@@ -137,9 +137,8 @@ Section iris_tests.
   Lemma test_iInv_4_with_close t N E1 E2 P:
     â†‘N âŠ† E2 â†’
     na_inv t N (<pers> P) âˆ— na_own t E1 âˆ— na_own t E2
-         âŠ¢ |={âŠ¤}=> na_own t E1 âˆ— na_own t E2  âˆ— â–· P.
+         ={âŠ¤}=âˆ— na_own t E1 âˆ— na_own t E2  âˆ— â–· P.
   Proof.
-    Show.
     iIntros (?) "(#?&Hown1&Hown2)".
     iInv N as "(#HP&Hown2)" "Hclose". Show.
     iMod ("Hclose" with "[HP Hown2]").
-- 
GitLab