diff --git a/CHANGELOG.md b/CHANGELOG.md
index fcf3fe79a1ec3519a288c2db638d26c283b7371b..2ad4c79049417177c77fc533d1b1c5c03e95d29a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Renaming and moving things around: uPred and the rest of the base logic are
   in `base_logic`, while `program_logic` is for everything involving the
   general Iris notion of a language.
+* Changed notation for embedding Coq assertions into Iris.  The new notation
+  is âŒœÏ†âŒ.  Also removed `=` and `âŠ¥` from the Iris scope.
+  (The old notations are provided in `base_logic.deprecated`.)
 * With invariants and the physical state being handled in the logic, there
   is no longer any reason to demand the CMRA unit to be discrete.
 * The language can now fork off multiple threads at once.
diff --git a/_CoqProject b/_CoqProject
index 419e8982165db35e68851f2430f61ca38b03f356..2def8bf45928256ba05e84333c694af0c032892b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -68,6 +68,7 @@ base_logic/big_op.v
 base_logic/hlist.v
 base_logic/soundness.v
 base_logic/double_negation.v
+base_logic/deprecated.v
 base_logic/lib/iprop.v
 base_logic/lib/own.v
 base_logic/lib/saved_prop.v
diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index 5ac30fc76e235916ebd900675e70c7afd082aaab..be9ae4df854446d2b7b6963d8a3d301e62043a33 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -252,7 +252,7 @@ Section list.
 
   Lemma big_sepL_forall Î¦ l :
     (âˆ€ k x, PersistentP (Î¦ k x)) â†’
-    ([âˆ— list] kâ†¦x âˆˆ l, Î¦ k x) âŠ£âŠ¢ (âˆ€ k x, l !! k = Some x â†’ Î¦ k x).
+    ([âˆ— list] kâ†¦x âˆˆ l, Î¦ k x) âŠ£âŠ¢ (âˆ€ k x, âŒœl !! k = Some xâŒ â†’ Î¦ k x).
   Proof.
     intros HÎ¦. apply (anti_symm _).
     { apply forall_intro=> k; apply forall_intro=> x.
@@ -265,7 +265,7 @@ Section list.
   Qed.
 
   Lemma big_sepL_impl Î¦ Î¨ l :
-    â–¡ (âˆ€ k x, l !! k = Some x â†’ Î¦ k x â†’ Î¨ k x) âˆ§ ([âˆ— list] kâ†¦x âˆˆ l, Î¦ k x)
+    â–¡ (âˆ€ k x, âŒœl !! k = Some xâŒ â†’ Î¦ k x â†’ Î¨ k x) âˆ§ ([âˆ— list] kâ†¦x âˆˆ l, Î¦ k x)
     âŠ¢ [âˆ— list] kâ†¦x âˆˆ l, Î¨ k x.
   Proof.
     rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
@@ -376,7 +376,7 @@ Section gmap.
 
   Lemma big_sepM_forall Î¦ m :
     (âˆ€ k x, PersistentP (Î¦ k x)) â†’
-    ([âˆ— map] kâ†¦x âˆˆ m, Î¦ k x) âŠ£âŠ¢ (âˆ€ k x, m !! k = Some x â†’ Î¦ k x).
+    ([âˆ— map] kâ†¦x âˆˆ m, Î¦ k x) âŠ£âŠ¢ (âˆ€ k x, âŒœm !! k = Some xâŒ â†’ Î¦ k x).
   Proof.
     intros. apply (anti_symm _).
     { apply forall_intro=> k; apply forall_intro=> x.
@@ -392,7 +392,7 @@ Section gmap.
   Qed.
 
   Lemma big_sepM_impl Î¦ Î¨ m :
-    â–¡ (âˆ€ k x, m !! k = Some x â†’ Î¦ k x â†’ Î¨ k x) âˆ§ ([âˆ— map] kâ†¦x âˆˆ m, Î¦ k x)
+    â–¡ (âˆ€ k x, âŒœm !! k = Some xâŒ â†’ Î¦ k x â†’ Î¨ k x) âˆ§ ([âˆ— map] kâ†¦x âˆˆ m, Î¦ k x)
     âŠ¢ [âˆ— map] kâ†¦x âˆˆ m, Î¨ k x.
   Proof.
     rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
@@ -473,7 +473,7 @@ Section gset.
   Proof. apply: big_opS_singleton. Qed.
 
   Lemma big_sepS_filter (P : A â†’ Prop) `{âˆ€ x, Decision (P x)} Î¦ X :
-    ([âˆ— set] y âˆˆ filter P X, Î¦ y) âŠ£âŠ¢ ([âˆ— set] y âˆˆ X, â–  P y â†’ Î¦ y).
+    ([âˆ— set] y âˆˆ filter P X, Î¦ y) âŠ£âŠ¢ ([âˆ— set] y âˆˆ X, âŒœP yâŒ â†’ Î¦ y).
   Proof.
     induction X as [|x X ? IH] using collection_ind_L.
     { by rewrite filter_empty_L !big_sepS_empty. }
@@ -500,7 +500,7 @@ Section gset.
   Proof. apply (big_opS_commute _). Qed.
 
   Lemma big_sepS_forall Î¦ X :
-    (âˆ€ x, PersistentP (Î¦ x)) â†’ ([âˆ— set] x âˆˆ X, Î¦ x) âŠ£âŠ¢ (âˆ€ x, â–  (x âˆˆ X) â†’ Î¦ x).
+    (âˆ€ x, PersistentP (Î¦ x)) â†’ ([âˆ— set] x âˆˆ X, Î¦ x) âŠ£âŠ¢ (âˆ€ x, âŒœx âˆˆ XâŒ â†’ Î¦ x).
   Proof.
     intros. apply (anti_symm _).
     { apply forall_intro=> x.
@@ -514,7 +514,7 @@ Section gset.
   Qed.
 
   Lemma big_sepS_impl Î¦ Î¨ X :
-    â–¡ (âˆ€ x, â–  (x âˆˆ X) â†’ Î¦ x â†’ Î¨ x) âˆ§ ([âˆ— set] x âˆˆ X, Î¦ x) âŠ¢ [âˆ— set] x âˆˆ X, Î¨ x.
+    â–¡ (âˆ€ x, âŒœx âˆˆ XâŒ â†’ Î¦ x â†’ Î¨ x) âˆ§ ([âˆ— set] x âˆˆ X, Î¦ x) âŠ¢ [âˆ— set] x âˆˆ X, Î¨ x.
   Proof.
     rewrite always_and_sep_l always_forall.
     setoid_rewrite always_impl; setoid_rewrite always_pure.
diff --git a/base_logic/deprecated.v b/base_logic/deprecated.v
new file mode 100644
index 0000000000000000000000000000000000000000..01ac005776b55ffc2a947e9a4ffe2bac17b9b9ce
--- /dev/null
+++ b/base_logic/deprecated.v
@@ -0,0 +1,11 @@
+From iris.base_logic Require Import primitive.
+
+(* Deprecated 2016-11-22. Use âŒœÏ†âŒ instead. *)
+Notation "â–  Ï†" := (uPred_pure Ï†%C%type)
+    (at level 20, right associativity, only parsing) : uPred_scope.
+
+(* Deprecated 2016-11-22. Use âŒœx = yâŒ instead. *)
+Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) (only parsing) : uPred_scope.
+
+(* Deprecated 2016-11-22. Use âŒœx âŠ¥ y âŒ instead. *)
+Notation "x âŠ¥ y" := (uPred_pure (x%C%type âŠ¥ y%C%type)) (only parsing) : uPred_scope.
diff --git a/base_logic/derived.v b/base_logic/derived.v
index b822512b4897c48ff6a9e73718a3613d92a98137..0f4de13f4355ab08f2a44fe2b0d19e49d5c1f703 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -212,53 +212,53 @@ Proof.
   - apply or_elim; apply exist_elim=> a; rewrite -(exist_intro a); auto.
 Qed.
 
-Lemma pure_mono Ï†1 Ï†2 : (Ï†1 â†’ Ï†2) â†’ â–  Ï†1 âŠ¢ â–  Ï†2.
+Lemma pure_mono Ï†1 Ï†2 : (Ï†1 â†’ Ï†2) â†’ âŒœÏ†1âŒ âŠ¢ âŒœÏ†2âŒ.
 Proof. intros; apply pure_elim with Ï†1; eauto. Qed.
 Global Instance pure_mono' : Proper (impl ==> (âŠ¢)) (@uPred_pure M).
 Proof. intros Ï†1 Ï†2; apply pure_mono. Qed.
-Lemma pure_iff Ï†1 Ï†2 : (Ï†1 â†” Ï†2) â†’ â–  Ï†1 âŠ£âŠ¢ â–  Ï†2.
+Lemma pure_iff Ï†1 Ï†2 : (Ï†1 â†” Ï†2) â†’ âŒœÏ†1âŒ âŠ£âŠ¢ âŒœÏ†2âŒ.
 Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
-Lemma pure_intro_l Ï† Q R : Ï† â†’ (â–  Ï† âˆ§ Q âŠ¢ R) â†’ Q âŠ¢ R.
+Lemma pure_intro_l Ï† Q R : Ï† â†’ (âŒœÏ†âŒ âˆ§ Q âŠ¢ R) â†’ Q âŠ¢ R.
 Proof. intros ? <-; auto using pure_intro. Qed.
-Lemma pure_intro_r Ï† Q R : Ï† â†’ (Q âˆ§ â–  Ï† âŠ¢ R) â†’ Q âŠ¢ R.
+Lemma pure_intro_r Ï† Q R : Ï† â†’ (Q âˆ§ âŒœÏ†âŒ âŠ¢ R) â†’ Q âŠ¢ R.
 Proof. intros ? <-; auto. Qed.
-Lemma pure_intro_impl Ï† Q R : Ï† â†’ (Q âŠ¢ â–  Ï† â†’ R) â†’ Q âŠ¢ R.
+Lemma pure_intro_impl Ï† Q R : Ï† â†’ (Q âŠ¢ âŒœÏ†âŒ â†’ R) â†’ Q âŠ¢ R.
 Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
-Lemma pure_elim_l Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ â–  Ï† âˆ§ Q âŠ¢ R.
+Lemma pure_elim_l Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ âŒœÏ†âŒ âˆ§ Q âŠ¢ R.
 Proof. intros; apply pure_elim with Ï†; eauto. Qed.
-Lemma pure_elim_r Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ Q âˆ§ â–  Ï† âŠ¢ R.
+Lemma pure_elim_r Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ Q âˆ§ âŒœÏ†âŒ âŠ¢ R.
 Proof. intros; apply pure_elim with Ï†; eauto. Qed.
 
-Lemma pure_True (Ï† : Prop) : Ï† â†’ â–  Ï† âŠ£âŠ¢ True.
+Lemma pure_True (Ï† : Prop) : Ï† â†’ âŒœÏ†âŒ âŠ£âŠ¢ True.
 Proof. intros; apply (anti_symm _); auto. Qed.
-Lemma pure_False (Ï† : Prop) : Â¬Ï† â†’ â–  Ï† âŠ£âŠ¢ False.
+Lemma pure_False (Ï† : Prop) : Â¬Ï† â†’ âŒœÏ†âŒ âŠ£âŠ¢ False.
 Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed.
 
-Lemma pure_and Ï†1 Ï†2 : â–  (Ï†1 âˆ§ Ï†2) âŠ£âŠ¢ â–  Ï†1 âˆ§ â–  Ï†2.
+Lemma pure_and Ï†1 Ï†2 : âŒœÏ†1 âˆ§ Ï†2âŒ âŠ£âŠ¢ âŒœÏ†1âŒ âˆ§ âŒœÏ†2âŒ.
 Proof.
   apply (anti_symm _).
   - eapply pure_elim=> // -[??]; auto.
   - eapply (pure_elim Ï†1); [auto|]=> ?. eapply (pure_elim Ï†2); auto.
 Qed.
-Lemma pure_or Ï†1 Ï†2 : â–  (Ï†1 âˆ¨ Ï†2) âŠ£âŠ¢ â–  Ï†1 âˆ¨ â–  Ï†2.
+Lemma pure_or Ï†1 Ï†2 : âŒœÏ†1 âˆ¨ Ï†2âŒ âŠ£âŠ¢ âŒœÏ†1âŒ âˆ¨ âŒœÏ†2âŒ.
 Proof.
   apply (anti_symm _).
   - eapply pure_elim=> // -[?|?]; auto.
   - apply or_elim; eapply pure_elim; eauto.
 Qed.
-Lemma pure_impl Ï†1 Ï†2 : â–  (Ï†1 â†’ Ï†2) âŠ£âŠ¢ (â–  Ï†1 â†’ â–  Ï†2).
+Lemma pure_impl Ï†1 Ï†2 : âŒœÏ†1 â†’ Ï†2âŒ âŠ£âŠ¢ (âŒœÏ†1âŒ â†’ âŒœÏ†2âŒ).
 Proof.
   apply (anti_symm _).
   - apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
   - rewrite -pure_forall_2. apply forall_intro=> ?.
     by rewrite -(left_id True uPred_and (_â†’_))%I (pure_True Ï†1) // impl_elim_r.
 Qed.
-Lemma pure_forall {A} (Ï† : A â†’ Prop) : â–  (âˆ€ x, Ï† x) âŠ£âŠ¢ âˆ€ x, â–  Ï† x.
+Lemma pure_forall {A} (Ï† : A â†’ Prop) : âŒœâˆ€ x, Ï† xâŒ âŠ£âŠ¢ âˆ€ x, âŒœÏ† xâŒ.
 Proof.
   apply (anti_symm _); auto using pure_forall_2.
   apply forall_intro=> x. eauto using pure_mono.
 Qed.
-Lemma pure_exist {A} (Ï† : A â†’ Prop) : â–  (âˆƒ x, Ï† x) âŠ£âŠ¢ âˆƒ x, â–  Ï† x.
+Lemma pure_exist {A} (Ï† : A â†’ Prop) : âŒœâˆƒ x, Ï† xâŒ âŠ£âŠ¢ âˆƒ x, âŒœÏ† xâŒ.
 Proof.
   apply (anti_symm _).
   - eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto.
@@ -273,13 +273,13 @@ Proof. by intros ->. Qed.
 Lemma internal_eq_sym {A : ofeT} (a b : A) : a â‰¡ b âŠ¢ b â‰¡ a.
 Proof. apply (internal_eq_rewrite a b (Î» b, b â‰¡ a)%I); auto. solve_proper. Qed.
 
-Lemma pure_impl_forall Ï† P : (â–  Ï† â†’ P) âŠ£âŠ¢ (âˆ€ _ : Ï†, P).
+Lemma pure_impl_forall Ï† P : (âŒœÏ†âŒ â†’ P) âŠ£âŠ¢ (âˆ€ _ : Ï†, P).
 Proof.
   apply (anti_symm _).
   - apply forall_intro=> ?. by rewrite pure_True // left_id.
   - apply impl_intro_l, pure_elim_l=> HÏ†. by rewrite (forall_elim HÏ†).
 Qed.
-Lemma pure_alt Ï† : â–  Ï† âŠ£âŠ¢ âˆƒ _ : Ï†, True.
+Lemma pure_alt Ï† : âŒœÏ†âŒ âŠ£âŠ¢ âˆƒ _ : Ï†, True.
 Proof.
   apply (anti_symm _).
   - eapply pure_elim; eauto=> H. rewrite -(exist_intro H); auto.
@@ -406,9 +406,9 @@ Lemma sep_and P Q : (P âˆ— Q) âŠ¢ (P âˆ§ Q).
 Proof. auto. Qed.
 Lemma impl_wand P Q : (P â†’ Q) âŠ¢ P -âˆ— Q.
 Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
-Lemma pure_elim_sep_l Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ â–  Ï† âˆ— Q âŠ¢ R.
+Lemma pure_elim_sep_l Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ âŒœÏ†âŒ âˆ— Q âŠ¢ R.
 Proof. intros; apply pure_elim with Ï†; eauto. Qed.
-Lemma pure_elim_sep_r Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ Q âˆ— â–  Ï† âŠ¢ R.
+Lemma pure_elim_sep_r Ï† Q R : (Ï† â†’ Q âŠ¢ R) â†’ Q âˆ— âŒœÏ†âŒ âŠ¢ R.
 Proof. intros; apply pure_elim with Ï†; eauto. Qed.
 
 Global Instance sep_False : LeftAbsorb (âŠ£âŠ¢) False%I (@uPred_sep M).
@@ -452,7 +452,7 @@ Proof. intros P Q; apply always_mono. Qed.
 Lemma always_intro' P Q : (â–¡ P âŠ¢ Q) â†’ â–¡ P âŠ¢ â–¡ Q.
 Proof. intros <-. apply always_idemp. Qed.
 
-Lemma always_pure Ï† : â–¡ â–  Ï† âŠ£âŠ¢ â–  Ï†.
+Lemma always_pure Ï† : â–¡ âŒœÏ†âŒ âŠ£âŠ¢ âŒœÏ†âŒ.
 Proof. apply (anti_symm _); auto using always_pure_2. Qed.
 Lemma always_forall {A} (Î¨ : A â†’ uPred M) : (â–¡ âˆ€ a, Î¨ a) âŠ£âŠ¢ (âˆ€ a, â–¡ Î¨ a).
 Proof.
@@ -560,7 +560,7 @@ Proof. destruct p; simpl; auto using always_elim. Qed.
 Lemma always_elim_if p P : â–¡ P âŠ¢ â–¡?p P.
 Proof. destruct p; simpl; auto using always_elim. Qed.
 
-Lemma always_if_pure p Ï† : â–¡?p â–  Ï† âŠ£âŠ¢ â–  Ï†.
+Lemma always_if_pure p Ï† : â–¡?p âŒœÏ†âŒ âŠ£âŠ¢ âŒœÏ†âŒ.
 Proof. destruct p; simpl; auto using always_pure. Qed.
 Lemma always_if_and p P Q : â–¡?p (P âˆ§ Q) âŠ£âŠ¢ â–¡?p P âˆ§ â–¡?p Q.
 Proof. destruct p; simpl; auto using always_and. Qed.
@@ -663,7 +663,7 @@ Proof.
 Qed.
 
 (* Timeless instances *)
-Global Instance pure_timeless Ï† : TimelessP (â–  Ï† : uPred M)%I.
+Global Instance pure_timeless Ï† : TimelessP (âŒœÏ†âŒ : uPred M)%I.
 Proof.
   rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
 Qed.
@@ -725,7 +725,7 @@ Proof.
 Qed.
 
 (* Persistence *)
-Global Instance pure_persistent Ï† : PersistentP (â–  Ï† : uPred M)%I.
+Global Instance pure_persistent Ï† : PersistentP (âŒœÏ†âŒ : uPred M)%I.
 Proof. by rewrite /PersistentP always_pure. Qed.
 Global Instance always_persistent P : PersistentP (â–¡ P).
 Proof. by intros; apply always_intro'. Qed.
diff --git a/base_logic/double_negation.v b/base_logic/double_negation.v
index e73d0d078b5527b42375e43f06413deb1f88d96b..52ae21612b3605693fddf51f66caf3250b67a327 100644
--- a/base_logic/double_negation.v
+++ b/base_logic/double_negation.v
@@ -36,7 +36,7 @@ Implicit Types x : M.
 Import uPred.
 
 (* Helper lemmas about iterated later modalities *)
-Lemma laterN_big n a x Ï†: âœ“{n} x â†’  a â‰¤ n â†’ (â–·^a (â–  Ï†))%I n x â†’ Ï†.
+Lemma laterN_big n a x Ï†: âœ“{n} x â†’  a â‰¤ n â†’ (â–·^a âŒœÏ†âŒ)%I n x â†’ Ï†.
 Proof.
   induction 2 as [| ?? IHle].
   - induction a; repeat (rewrite //= || uPred.unseal). 
@@ -46,7 +46,7 @@ Proof.
     eapply uPred_closed; eauto using cmra_validN_S.
 Qed.
 
-Lemma laterN_small n a x Ï†: âœ“{n} x â†’  n < a â†’ (â–·^a (â–  Ï†))%I n x.
+Lemma laterN_small n a x Ï†: âœ“{n} x â†’  n < a â†’ (â–·^a âŒœÏ†âŒ)%I n x.
 Proof.
   induction 2.
   - induction n as [| n IHn]; [| move: IHn];
@@ -85,7 +85,7 @@ Proof.
   by rewrite -assoc wand_elim_r wand_elim_l.
 Qed.
 Lemma nnupd_ownM_updateP x (Î¦ : M â†’ Prop) :
-  x ~~>: Î¦ â†’ uPred_ownM x =n=> âˆƒ y, â–  Î¦ y âˆ§ uPred_ownM y.
+  x ~~>: Î¦ â†’ uPred_ownM x =n=> âˆƒ y, âŒœÎ¦ yâŒ âˆ§ uPred_ownM y.
 Proof. 
   intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal. 
   intros n y ? Hown a.
@@ -306,7 +306,7 @@ End classical.
    we establish adequacy without axioms? Unfortunately not, because adequacy for 
    nnupd would imply double negation elimination, which is classical: *)
 
-Lemma nnupd_dne Ï†: True âŠ¢ (|=n=> (â– (Â¬Â¬ Ï† â†’ Ï†)): uPred M)%I.
+Lemma nnupd_dne Ï†: True âŠ¢ (|=n=> âŒœÂ¬Â¬ Ï† â†’ Ï†âŒ: uPred M)%I.
 Proof.
   rewrite /uPred_nnupd. apply forall_intro=>n.
   apply wand_intro_l. rewrite ?right_id. 
@@ -358,9 +358,9 @@ Proof.
     eapply IHn; eauto.
 Qed.
 
-Lemma adequacy Ï† n : (True âŠ¢ Nat.iter n (Î» P, |=n=> â–· P) (â–  Ï†)) â†’ Â¬Â¬ Ï†.
+Lemma adequacy Ï† n : (True âŠ¢ Nat.iter n (Î» P, |=n=> â–· P) âŒœÏ†âŒ) â†’ Â¬Â¬ Ï†.
 Proof.
-  cut (âˆ€ x, âœ“{S n} x â†’ Nat.iter n (Î» P, |=n=> â–· P)%I (â–  Ï†)%I (S n) x â†’ Â¬Â¬Ï†).
+  cut (âˆ€ x, âœ“{S n} x â†’ Nat.iter n (Î» P, |=n=> â–· P)%I âŒœÏ†âŒ%I (S n) x â†’ Â¬Â¬Ï†).
   { intros help H. eapply (help âˆ…); eauto using ucmra_unit_validN.
     eapply H; try unseal; eauto using ucmra_unit_validN. red; rewrite //=. }
   destruct n.
diff --git a/base_logic/lib/auth.v b/base_logic/lib/auth.v
index c0dbaff19c5930a7d02abb007d236c0dcc98ff31..30054193777ee2356abffd6e09498ff36b177dbb 100644
--- a/base_logic/lib/auth.v
+++ b/base_logic/lib/auth.v
@@ -92,7 +92,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.
     iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (Î³) "[% HÎ³]"; first done.
@@ -114,8 +114,8 @@ Section auth.
 
   Lemma auth_acc E Î³ a :
     â–· 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.
+      âŒœa â‰¼ f tâŒ âˆ— â–· Ï† t âˆ— âˆ€ u b,
+      âŒœ(f t, a) ~l~> (f u, b)âŒ âˆ— â–· Ï† u ={E}=âˆ— â–· auth_inv Î³ f Ï† âˆ— auth_own Î³ b.
   Proof.
     iIntros "[Hinv HÎ³f]". rewrite /auth_inv /auth_own.
     iDestruct "Hinv" as (t) "[>HÎ³a HÏ†]".
@@ -130,8 +130,8 @@ Section auth.
   Lemma auth_open E N Î³ a :
     nclose N âŠ† E â†’
     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.
+      âŒœa â‰¼ f tâŒ âˆ— â–· Ï† t âˆ— âˆ€ u b,
+      âŒœ(f t, a) ~l~> (f u, b)âŒ âˆ— â–· Ï† u ={Eâˆ–N,E}=âˆ— auth_own Î³ b.
   Proof.
     iIntros (?) "[#? HÎ³f]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
     (* The following is essentially a very trivial composition of the accessors
diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 0327ca20bd13e06d4258791a63419c1c5c8b7ab1..cd2f1f8fc336fd54dfde1e83003e418c0501947d 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -55,7 +55,7 @@ Global Instance slice_persistent Î³ P : PersistentP (slice N Î³ P).
 Proof. apply _. Qed.
 
 Lemma box_own_auth_agree Î³ b1 b2 :
-  box_own_auth Î³ (â— Excl' b1) âˆ— box_own_auth Î³ (â—¯ Excl' b2) âŠ¢ b1 = b2.
+  box_own_auth Î³ (â— Excl' b1) âˆ— box_own_auth Î³ (â—¯ Excl' b2) âŠ¢ âŒœb1 = b2âŒ.
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
   by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
@@ -86,7 +86,7 @@ Proof.
 Qed.
 
 Lemma box_insert E f P Q :
-  â–· box N f P ={E}=âˆ— âˆƒ Î³, f !! Î³ = None âˆ—
+  â–· box N f P ={E}=âˆ— âˆƒ Î³, âŒœf !! Î³ = NoneâŒ âˆ—
     slice N Î³ Q âˆ— â–· box N (<[Î³:=false]> f) (Q âˆ— P).
 Proof.
   iDestruct 1 as (Î¦) "[#HeqP Hf]".
diff --git a/base_logic/lib/fancy_updates.v b/base_logic/lib/fancy_updates.v
index e36059cc4c08c9d1d85757312c78cc8ae49f6e5d..2db972b93352cac1a706246b152681ff2a18009e 100644
--- a/base_logic/lib/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -69,7 +69,7 @@ Proof.
 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)".
   iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
diff --git a/base_logic/lib/invariants.v b/base_logic/lib/invariants.v
index 4fd9016fa1256379955df8c8da6cd80b63b01930..14e4fff3123d852eeabc03428f71acab1a487c63 100644
--- a/base_logic/lib/invariants.v
+++ b/base_logic/lib/invariants.v
@@ -6,7 +6,7 @@ Import uPred.
 
 (** Derived forms and lemmas about them. *)
 Definition inv_def `{invG Î£} (N : namespace) (P : iProp Î£) : iProp Î£ :=
-  (âˆƒ i, â–  (i âˆˆ nclose N) âˆ§ ownI i P)%I.
+  (âˆƒ i, âŒœi âˆˆ nclose NâŒ âˆ§ ownI i P)%I.
 Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
 Definition inv {Î£ i} := proj1_sig inv_aux Î£ i.
 Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
diff --git a/base_logic/lib/own.v b/base_logic/lib/own.v
index 1e320bcaf1b8f5230118b8b21cc545aa71b623dc..161ec78952eda4be74797330ec7e1a4783876809 100644
--- a/base_logic/lib/own.v
+++ b/base_logic/lib/own.v
@@ -86,10 +86,10 @@ 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 ==âˆ— âˆƒ Î³, â–  (Î³ âˆ‰ G) âˆ§ own Î³ a.
+  âœ“ a â†’ True ==âˆ— âˆƒ Î³, âŒœÎ³ âˆ‰ GâŒ âˆ§ own Î³ a.
 Proof.
   intros Ha.
-  rewrite -(bupd_mono (âˆƒ m, â–  (âˆƒ Î³, Î³ âˆ‰ G âˆ§ m = iRes_singleton Î³ a) âˆ§ uPred_ownM m)%I).
+  rewrite -(bupd_mono (âˆƒ m, âŒœâˆƒ Î³, Î³ âˆ‰ G âˆ§ m = iRes_singleton Î³ aâŒ âˆ§ uPred_ownM m)%I).
   - rewrite ownM_empty.
     eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (inG_id _));
       first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
@@ -104,10 +104,10 @@ Proof.
 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 Ha. rewrite !own_eq.
-  rewrite -(bupd_mono (âˆƒ m, â–  (âˆƒ a', m = iRes_singleton Î³ a' âˆ§ P a') âˆ§ uPred_ownM m)%I).
+  rewrite -(bupd_mono (âˆƒ m, âŒœâˆƒ a', m = iRes_singleton Î³ a' âˆ§ P a'âŒ âˆ§ uPred_ownM m)%I).
   - eapply bupd_ownM_updateP, iprod_singleton_updateP;
       first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
     naive_solver.
diff --git a/base_logic/lib/saved_prop.v b/base_logic/lib/saved_prop.v
index 533fd52e2bc97a43f6caec84ed3f2fd0dfe65a9f..a61912f876c630784fe22b4a5db17771db6ad1f4 100644
--- a/base_logic/lib/saved_prop.v
+++ b/base_logic/lib/saved_prop.v
@@ -26,7 +26,7 @@ Section saved_prop.
   Proof. rewrite /saved_prop_own; apply _. Qed.
 
   Lemma saved_prop_alloc_strong x (G : gset gname) :
-    True ==âˆ— âˆƒ Î³, â–  (Î³ âˆ‰ G) âˆ§ saved_prop_own Î³ x.
+    True ==âˆ— âˆƒ Î³, âŒœÎ³ âˆ‰ GâŒ âˆ§ saved_prop_own Î³ x.
   Proof. by apply own_alloc_strong. Qed.
 
   Lemma saved_prop_alloc x : True ==âˆ— âˆƒ Î³, saved_prop_own Î³ x.
diff --git a/base_logic/lib/sts.v b/base_logic/lib/sts.v
index 6ba8f98fba41d23b64ab0e227aef8c9d7c435030..15299e9bef424db149d36d7b06d6f14638a342cc 100644
--- a/base_logic/lib/sts.v
+++ b/base_logic/lib/sts.v
@@ -94,8 +94,8 @@ Section sts.
 
   Lemma sts_accS E Î³ S T :
     â–· 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'.
+      âŒœs âˆˆ SâŒ âˆ— â–· Ï† s âˆ— âˆ€ s' T',
+      âŒœsts.steps (s, T) (s', T')âŒ âˆ— â–· Ï† s' ={E}=âˆ— â–· sts_inv Î³ Ï† âˆ— sts_own Î³ s' T'.
   Proof.
     iIntros "[Hinv HÎ³f]". rewrite /sts_ownS /sts_inv /sts_own.
     iDestruct "Hinv" as (s) "[>HÎ³ HÏ†]".
@@ -112,15 +112,15 @@ Section sts.
 
   Lemma sts_acc E Î³ s0 T :
     â–· 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'.
+      âŒœ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,
-      â–  (s âˆˆ S) âˆ— â–· Ï† s âˆ— âˆ€ s' T',
-      â–  sts.steps (s, T) (s', T') âˆ— â–· Ï† s' ={Eâˆ–N,E}=âˆ— sts_own Î³ s' T'.
+      âŒœs âˆˆ SâŒ âˆ— â–· Ï† s âˆ— âˆ€ s' T',
+      âŒœsts.steps (s, T) (s', T')âŒ âˆ— â–· Ï† s' ={Eâˆ–N,E}=âˆ— sts_own Î³ s' T'.
   Proof.
     iIntros (?) "[#? HÎ³f]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
     (* The following is essentially a very trivial composition of the accessors
@@ -137,7 +137,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.frame_steps T s0 s) âˆ— â–· Ï† s âˆ— âˆ€ s' T',
-      â–  (sts.steps (s, T) (s', T')) âˆ— â–· Ï† s' ={Eâˆ–N,E}=âˆ— sts_own Î³ s' T'.
+      âŒœ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.
 End sts.
diff --git a/base_logic/lib/thread_local.v b/base_logic/lib/thread_local.v
index 57b65ac024bd952136c410547ae715a989776ea6..c97d31f212753a15bf3c74d536a1d454b0038a72 100644
--- a/base_logic/lib/thread_local.v
+++ b/base_logic/lib/thread_local.v
@@ -16,7 +16,7 @@ Section defs.
     own tid (CoPset E, âˆ…).
 
   Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Î£) : iProp Î£ :=
-    (âˆƒ i, â–  (i âˆˆ nclose N) âˆ§
+    (âˆƒ i, âŒœi âˆˆ nclose NâŒ âˆ§
           inv tlN (P âˆ— own tid (âˆ…, GSet {[i]}) âˆ¨ tl_own tid {[i]}))%I.
 End defs.
 
@@ -40,7 +40,7 @@ Section proofs.
   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).
+  Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 âˆ— tl_own tid E2 âŠ¢ âŒœE1 âŠ¥ E2âŒ.
   Proof.
     rewrite /tl_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
   Qed.
diff --git a/base_logic/lib/wsat.v b/base_logic/lib/wsat.v
index d3498adb6348c2ff5ff9dc5fcabf8ac0667d885e..b75702333615083123601d5df3705813a176ef9e 100644
--- a/base_logic/lib/wsat.v
+++ b/base_logic/lib/wsat.v
@@ -56,9 +56,9 @@ Lemma ownE_empty : True ==âˆ— ownE âˆ….
 Proof. by rewrite (own_empty (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.
-Lemma ownE_disjoint E1 E2 : ownE E1 âˆ— ownE E2 âŠ¢ E1 âŠ¥ E2.
+Lemma ownE_disjoint E1 E2 : ownE E1 âˆ— ownE E2 âŠ¢ âŒœE1 âŠ¥ E2âŒ.
 Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed.
-Lemma ownE_op' E1 E2 : E1 âŠ¥ E2 âˆ§ ownE (E1 âˆª E2) âŠ£âŠ¢ ownE E1 âˆ— ownE E2.
+Lemma ownE_op' E1 E2 : âŒœE1 âŠ¥ E2âŒ âˆ§ ownE (E1 âˆª E2) âŠ£âŠ¢ ownE E1 âˆ— ownE E2.
 Proof.
   iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
   iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?.
@@ -71,9 +71,9 @@ Lemma ownD_empty : True ==âˆ— ownD âˆ….
 Proof. by rewrite (own_empty (gset_disjUR positive) 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.
-Lemma ownD_disjoint E1 E2 : ownD E1 âˆ— ownD E2 âŠ¢ E1 âŠ¥ E2.
+Lemma ownD_disjoint E1 E2 : ownD E1 âˆ— ownD E2 âŠ¢ âŒœE1 âŠ¥ E2âŒ.
 Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
-Lemma ownD_op' E1 E2 : E1 âŠ¥ E2 âˆ§ ownD (E1 âˆª E2) âŠ£âŠ¢ ownD E1 âˆ— ownD E2.
+Lemma ownD_op' E1 E2 : âŒœE1 âŠ¥ E2âŒ âˆ§ ownD (E1 âˆª E2) âŠ£âŠ¢ ownD E1 âˆ— ownD E2.
 Proof.
   iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
   iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?.
@@ -85,7 +85,7 @@ Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.
 Lemma invariant_lookup (I : gmap positive (iProp Î£)) i P :
   own invariant_name (â— (invariant_unfold <$> I : gmap _ _)) âˆ—
   own invariant_name (â—¯ {[i := invariant_unfold P]}) âŠ¢
-  âˆƒ Q, I !! i = Some Q âˆ— â–· (Q â‰¡ P).
+  âˆƒ Q, âŒœI !! i = Some QâŒ âˆ— â–· (Q â‰¡ P).
 Proof.
   rewrite -own_op own_valid auth_validI /=. iIntros "[#HI #HvI]".
   iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
@@ -123,7 +123,7 @@ Qed.
 
 Lemma ownI_alloc Ï† P :
   (âˆ€ E : gset positive, âˆƒ i, i âˆ‰ E âˆ§ Ï† i) â†’
-  wsat âˆ— â–· P ==âˆ— âˆƒ i, â–  (Ï† i) âˆ— wsat âˆ— ownI i P.
+  wsat âˆ— â–· P ==âˆ— âˆƒ i, âŒœÏ† iâŒ âˆ— wsat âˆ— ownI i P.
 Proof.
   iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
   iMod (own_empty (gset_disjUR positive) disabled_name) as "HE".
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index 0b26e7a38203145652cf817b00f9c1a0c6e3b579..c6c7565ea08058271ff1020a76661acd6439955b 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -155,10 +155,9 @@ Definition uPred_bupd_aux : { x | x = @uPred_bupd_def }. by eexists. Qed.
 Definition uPred_bupd {M} := proj1_sig uPred_bupd_aux M.
 Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := proj2_sig uPred_bupd_aux.
 
-Notation "â–  Ï†" := (uPred_pure Ï†%C%type)
-  (at level 20, right associativity) : uPred_scope.
-Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) : uPred_scope.
-Notation "x âŠ¥ y" := (uPred_pure (x%C%type âŠ¥ y%C%type)) : uPred_scope.
+(* Latest notation *)
+Notation "'âŒœ' Ï† 'âŒ'" := (uPred_pure Ï†%C%type)
+  (at level 1, Ï† at level 200, format "âŒœ Ï† âŒ") : uPred_scope.
 Notation "'False'" := (uPred_pure False) : uPred_scope.
 Notation "'True'" := (uPred_pure True) : uPred_scope.
 Infix "âˆ§" := uPred_and : uPred_scope.
@@ -317,13 +316,13 @@ Qed.
 Global Instance bupd_proper : Proper ((â‰¡) ==> (â‰¡)) (@uPred_bupd M) := ne_proper _.
 
 (** Introduction and elimination rules *)
-Lemma pure_intro Ï† P : Ï† â†’ P âŠ¢ â–  Ï†.
+Lemma pure_intro Ï† P : Ï† â†’ P âŠ¢ âŒœÏ†âŒ.
 Proof. by intros ?; unseal; split. Qed.
-Lemma pure_elim Ï† Q R : (Q âŠ¢ â–  Ï†) â†’ (Ï† â†’ Q âŠ¢ R) â†’ Q âŠ¢ R.
+Lemma pure_elim Ï† Q R : (Q âŠ¢ âŒœÏ†âŒ) â†’ (Ï† â†’ Q âŠ¢ R) â†’ Q âŠ¢ R.
 Proof.
   unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
 Qed.
-Lemma pure_forall_2 {A} (Ï† : A â†’ Prop) : (âˆ€ x : A, â–  Ï† x) âŠ¢ â–  (âˆ€ x : A, Ï† x).
+Lemma pure_forall_2 {A} (Ï† : A â†’ Prop) : (âˆ€ x : A, âŒœÏ† xâŒ) âŠ¢ âŒœâˆ€ x : A, Ï† xâŒ.
 Proof. by unseal. Qed.
 
 Lemma and_elim_l P Q : P âˆ§ Q âŠ¢ P.
@@ -426,7 +425,7 @@ Qed.
 Lemma always_idemp P : â–¡ P âŠ¢ â–¡ â–¡ P.
 Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
 
-Lemma always_pure_2 Ï† : â–  Ï† âŠ¢ â–¡ â–  Ï†.
+Lemma always_pure_2 Ï† : âŒœÏ†âŒ âŠ¢ â–¡ âŒœÏ†âŒ.
 Proof. by unseal. Qed.
 Lemma always_forall_2 {A} (Î¨ : A â†’ uPred M) : (âˆ€ a, â–¡ Î¨ a) âŠ¢ (â–¡ âˆ€ a, Î¨ a).
 Proof. by unseal. Qed.
@@ -542,7 +541,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 ==âˆ— âˆƒ 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 *.
@@ -562,9 +561,9 @@ Lemma later_equivI {A : ofeT} (x y : A) : Next x â‰¡ Next y âŠ£âŠ¢ â–· (x â‰¡ y)
 Proof. by unseal. Qed.
 
 (* Discrete *)
-Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : âœ“ a âŠ£âŠ¢ â–  âœ“ a.
+Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : âœ“ a âŠ£âŠ¢ âŒœâœ“ aâŒ.
 Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
-Lemma timeless_eq {A : ofeT} (a b : A) : Timeless a â†’ a â‰¡ b âŠ£âŠ¢ â–  (a â‰¡ b).
+Lemma timeless_eq {A : ofeT} (a b : A) : Timeless a â†’ a â‰¡ b âŠ£âŠ¢ âŒœa â‰¡ bâŒ.
 Proof.
   unseal=> ?. apply (anti_symm (âŠ¢)); split=> n x ?; by apply (timeless_iff n).
 Qed.
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 01aecda22ec0f9c94b1f160ec847a275b79e5afa..1e33e4054ccc349e7887bdbd503629740cde1801 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -16,7 +16,7 @@ Instance subG_heapPreG {Î£} : subG heapÎ£ Î£ â†’ heapPreG Î£.
 Proof. intros [? ?]%subG_inv. split; apply _. Qed.
 
 Definition heap_adequacy Î£ `{heapPreG Î£} e Ïƒ Ï† :
-  (âˆ€ `{heapG Î£}, heap_ctx âŠ¢ WP e {{ v, â–  Ï† v }}) â†’
+  (âˆ€ `{heapG Î£}, heap_ctx âŠ¢ WP e {{ v, âŒœÏ† vâŒ }}) â†’
   adequate e Ïƒ Ï†.
 Proof.
   intros Hwp; eapply (wp_adequacy Î£); iIntros (?) "HÏƒ".
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index a2b7d204328e0821cfcd6cba454eb7e0163303ef..45b4c8b584b9b61b0902afa127babf279fcc875e 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -85,7 +85,7 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_op l q1 q2 v1 v2 :
-    l â†¦{q1} v1 âˆ— l â†¦{q2} v2 âŠ£âŠ¢ v1 = v2 âˆ§ l â†¦{q1+q2} v1.
+    l â†¦{q1} v1 âˆ— l â†¦{q2} v2 âŠ£âŠ¢ âŒœv1 = v2âŒ âˆ§ l â†¦{q1+q2} v1.
   Proof.
     destruct (decide (v1 = v2)) as [->|].
     { by rewrite heap_mapsto_op_eq pure_True // left_id. }
@@ -96,15 +96,15 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_op_1 l q1 q2 v1 v2 :
-    l â†¦{q1} v1 âˆ— l â†¦{q2} v2 âŠ¢ v1 = v2 âˆ§ l â†¦{q1+q2} v1.
+    l â†¦{q1} v1 âˆ— l â†¦{q2} v2 âŠ¢ âŒœv1 = v2âŒ âˆ§ l â†¦{q1+q2} v1.
   Proof. by rewrite heap_mapsto_op. Qed.
 
   Lemma heap_mapsto_op_half l q v1 v2 :
-    l â†¦{q/2} v1 âˆ— l â†¦{q/2} v2 âŠ£âŠ¢ v1 = v2 âˆ§ l â†¦{q} v1.
+    l â†¦{q/2} v1 âˆ— l â†¦{q/2} v2 âŠ£âŠ¢ âŒœv1 = v2âŒ âˆ§ l â†¦{q} v1.
   Proof. by rewrite heap_mapsto_op Qp_div_2. Qed.
 
   Lemma heap_mapsto_op_half_1 l q v1 v2 :
-    l â†¦{q/2} v1 âˆ— l â†¦{q/2} v2 âŠ¢ v1 = v2 âˆ§ l â†¦{q} v1.
+    l â†¦{q/2} v1 âˆ— l â†¦{q/2} v2 âŠ¢ âŒœv1 = v2âŒ âˆ§ l â†¦{q} v1.
   Proof. by rewrite heap_mapsto_op_half. Qed.
 
   Lemma heap_ex_mapsto_op l q1 q2 : l â†¦{q1} - âˆ— l â†¦{q2} - âŠ£âŠ¢ l â†¦{q1+q2} -.
diff --git a/heap_lang/lib/assert.v b/heap_lang/lib/assert.v
index b222b908ddd29472e2f3aee7fadea1be89368a2e..547f961589011b808f2ad2867c196fda6c693380 100644
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
@@ -10,7 +10,7 @@ Notation "'assert:' e" := (assert (Î»: <>, e))%E (at level 99) : expr_scope.
 Global Opaque assert.
 
 Lemma wp_assert `{heapG Î£} E (Î¦ : val â†’ iProp Î£) e `{!Closed [] e} :
-  WP e @ E {{ v, v = #true âˆ§ â–· Î¦ #() }} âŠ¢ WP assert: e @ E {{ Î¦ }}.
+  WP e @ E {{ v, âŒœv = #trueâŒ âˆ§ â–· Î¦ #() }} âŠ¢ WP assert: e @ E {{ Î¦ }}.
 Proof.
   iIntros "HÎ¦". rewrite /assert. wp_let. wp_seq.
   iApply (wp_wand with "HÎ¦"). iIntros (v) "[% ?]"; subst. by wp_if.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index dc9ed307b6aa2212aa61569e557a5d0596feb89d..a859f60734b32d319834deb779d400dd33a47709 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -38,7 +38,7 @@ Definition barrier_inv (l : loc) (P : iProp Î£) (s : state) : iProp Î£ :=
   (l â†¦ s âˆ— ress (state_to_prop s P) (state_I s))%I.
 
 Definition barrier_ctx (Î³ : gname) (l : loc) (P : iProp Î£) : iProp Î£ :=
-  (â–  (heapN âŠ¥ N) âˆ— heap_ctx âˆ— sts_ctx Î³ N (barrier_inv l P))%I.
+  (âŒœheapN âŠ¥ NâŒ âˆ— heap_ctx âˆ— sts_ctx Î³ N (barrier_inv l P))%I.
 
 Definition send (l : loc) (P : iProp Î£) : iProp Î£ :=
   (âˆƒ Î³, barrier_ctx Î³ l P âˆ— sts_ownS Î³ low_states {[ Send ]})%I.
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index 914f97751df9f9ee99336578456ca4534a6d02d7..d5f581970f0c530587a1fd943592057712b5e436 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -11,7 +11,7 @@ Lemma barrier_spec (N : namespace) :
   heapN âŠ¥ N â†’
   âˆƒ recv send : loc â†’ iProp Î£ -n> iProp Î£,
     (âˆ€ P, heap_ctx âŠ¢ {{ True }} newbarrier #()
-                     {{ v, âˆƒ l : loc, v = #l âˆ— recv l P âˆ— send l P }}) âˆ§
+                     {{ v, âˆƒ l : loc, âŒœv = #lâŒ âˆ— recv l P âˆ— send l P }}) âˆ§
     (âˆ€ l P, {{ send l P âˆ— P }} signal #l {{ _, True }}) âˆ§
     (âˆ€ l P, {{ recv l P }} wait #l {{ _, P }}) âˆ§
     (âˆ€ l P Q, recv l (P âˆ— Q) ={N}=> recv l P âˆ— recv l Q) âˆ§
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index 8746e2b59466f94d7dd5c7b451342db0628a75b4..941ae644e63957e44b543b27efa22a42422477cf 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -26,7 +26,7 @@ Section mono_proof.
     (âˆƒ n, own Î³ (â— (n : mnat)) âˆ— l â†¦ #n)%I.
 
   Definition mcounter (l : loc) (n : nat) : iProp Î£ :=
-    (âˆƒ Î³, heapN âŠ¥ N âˆ§ heap_ctx âˆ§
+    (âˆƒ Î³, âŒœheapN âŠ¥ NâŒ âˆ§ heap_ctx âˆ§
           inv N (mcounter_inv Î³ l) âˆ§ own Î³ (â—¯ (n : mnat)))%I.
 
   (** The main proofs. *)
@@ -70,7 +70,7 @@ Section mono_proof.
   Qed.
 
   Lemma read_mono_spec l j :
-    {{{ mcounter l j }}} read #l {{{ i, RET #i; â–  (j â‰¤ i)%nat âˆ§ mcounter l i }}}.
+    {{{ mcounter l j }}} read #l {{{ i, RET #i; âŒœj â‰¤ iâŒ%nat âˆ§ mcounter l i }}}.
   Proof.
     iIntros (Ï•) "Hc HÎ¦". iDestruct "Hc" as (Î³) "(% & #? & #Hinv & HÎ³f)".
     rewrite /read /=. wp_let. iInv N as (c) ">[HÎ³ Hl]" "Hclose". wp_load.
@@ -99,7 +99,7 @@ Section contrib_spec.
     (âˆƒ n, own Î³ (â— Some (1%Qp, n)) âˆ— l â†¦ #n)%I.
 
   Definition ccounter_ctx (Î³ : gname) (l : loc) : iProp Î£ :=
-    (heapN âŠ¥ N âˆ§ heap_ctx âˆ§ inv N (ccounter_inv Î³ l))%I.
+    (âŒœheapN âŠ¥ NâŒ âˆ§ heap_ctx âˆ§ inv N (ccounter_inv Î³ l))%I.
 
   Definition ccounter (Î³ : gname) (q : frac) (n : nat) : iProp Î£ :=
     own Î³ (â—¯ Some (q, n)).
@@ -145,7 +145,7 @@ Section contrib_spec.
 
   Lemma read_contrib_spec Î³ l q n :
     {{{ ccounter_ctx Î³ l âˆ— ccounter Î³ q n }}} read #l
-    {{{ c, RET #c; â–  (n â‰¤ c)%nat âˆ§ ccounter Î³ q n }}}.
+    {{{ c, RET #c; âŒœn â‰¤ câŒ%nat âˆ§ ccounter Î³ q n }}}.
   Proof.
     iIntros (Î¦) "(#(%&?&?) & HÎ³f) HÎ¦".
     rewrite /read /=. wp_let. iInv N as (c) ">[HÎ³ Hl]" "Hclose". wp_load.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 8e2e167888eff87cd512bddc4f039b7e03a0c9ce..17c44630afcac7feefd5c13ff4b03a07efd62a03 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -29,11 +29,11 @@ Section proof.
 Context `{!heapG Î£, !spawnG Î£} (N : namespace).
 
 Definition spawn_inv (Î³ : gname) (l : loc) (Î¨ : val â†’ iProp Î£) : iProp Î£ :=
-  (âˆƒ lv, l â†¦ lv âˆ— (lv = NONEV âˆ¨
-                   âˆƒ v, lv = SOMEV v âˆ— (Î¨ v âˆ¨ own Î³ (Excl ()))))%I.
+  (âˆƒ lv, l â†¦ lv âˆ— (âŒœlv = NONEVâŒ âˆ¨
+                   âˆƒ v, âŒœlv = SOMEV vâŒ âˆ— (Î¨ v âˆ¨ own Î³ (Excl ()))))%I.
 
 Definition join_handle (l : loc) (Î¨ : val â†’ iProp Î£) : iProp Î£ :=
-  (heapN âŠ¥ N âˆ— âˆƒ Î³, heap_ctx âˆ— own Î³ (Excl ()) âˆ—
+  (âŒœheapN âŠ¥ NâŒ âˆ— âˆƒ Î³, heap_ctx âˆ— own Î³ (Excl ()) âˆ—
                     inv N (spawn_inv Î³ l Î¨))%I.
 
 Typeclasses Opaque join_handle.
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index d462f46a3e5b285e6b0a832758d8d143c0b10ce0..896caade9b443561c74bb15dde8cd87c44ba57dd 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -27,7 +27,7 @@ Section proof.
     (âˆƒ b : bool, l â†¦ #b âˆ— if b then True else own Î³ (Excl ()) âˆ— R)%I.
 
   Definition is_lock (Î³ : gname) (lk : val) (R : iProp Î£) : iProp Î£ :=
-    (âˆƒ l: loc, heapN âŠ¥ N âˆ§ heap_ctx âˆ§ lk = #l âˆ§ inv N (lock_inv Î³ l R))%I.
+    (âˆƒ l: loc, âŒœheapN âŠ¥ NâŒ âˆ§ heap_ctx âˆ§ âŒœlk = #lâŒ âˆ§ inv N (lock_inv Î³ l R))%I.
 
   Definition locked (Î³ : gname): iProp Î£ := own Î³ (Excl ()).
 
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 99543759d826294673a2ecd36f16875e8b3106ae..194b3da1f38fd94331f7b3b3a84c5b6d45409b98 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -47,13 +47,13 @@ Section proof.
 
   Definition is_lock (Î³ : gname) (lk : val) (R : iProp Î£) : iProp Î£ :=
     (âˆƒ lo ln : loc,
-       heapN âŠ¥ N âˆ§ heap_ctx âˆ§
-       lk = (#lo, #ln)%V âˆ§ inv N (lock_inv Î³ lo ln R))%I.
+       âŒœheapN âŠ¥ NâŒ âˆ§ heap_ctx âˆ§
+       âŒœlk = (#lo, #ln)%VâŒ âˆ§ inv N (lock_inv Î³ lo ln R))%I.
 
   Definition issued (Î³ : gname) (lk : val) (x : nat) (R : iProp Î£) : iProp Î£ :=
     (âˆƒ lo ln: loc,
-       heapN âŠ¥ N âˆ§ heap_ctx âˆ§
-       lk = (#lo, #ln)%V âˆ§ inv N (lock_inv Î³ lo ln R) âˆ§
+       âŒœheapN âŠ¥ NâŒ âˆ§ heap_ctx âˆ§
+       âŒœlk = (#lo, #ln)%VâŒ âˆ§ inv N (lock_inv Î³ lo ln R) âˆ§
        own Î³ (â—¯ (âˆ…, GSet {[ x ]})))%I.
 
   Definition locked (Î³ : gname) : iProp Î£ := (âˆƒ o, own Î³ (â—¯ (Excl' o, âˆ…)))%I.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 94a59db529c9896f69512be64f8daf5962eba93a..fbdde12b2e48fe0f023ad5605583392f6289b0d8 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -48,7 +48,7 @@ Proof. exact: weakestpre.wp_bind. Qed.
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E Ïƒ v :
   {{{ â–· ownP Ïƒ }}} Alloc (of_val v) @ E
-  {{{ l, RET LitV (LitLoc l); Ïƒ !! l = None âˆ§ ownP (<[l:=v]>Ïƒ) }}}.
+  {{{ l, RET LitV (LitLoc l); âŒœÏƒ !! l = NoneâŒ âˆ§ ownP (<[l:=v]>Ïƒ) }}}.
 Proof.
   iIntros (Î¦) "HP HÎ¦".
   iApply (wp_lift_atomic_head_step (Alloc (of_val v)) Ïƒ); eauto.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index c30f339bfc96606493c2b5e64885cea242e5025b..b789b798b695c46d81870e35ba05d638a8ff0b69 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -111,7 +111,7 @@ Qed.
 Lemma wptp_step e1 t1 t2 Ïƒ1 Ïƒ2 Î¦ :
   step (e1 :: t1,Ïƒ1) (t2, Ïƒ2) â†’
   world Ïƒ1 âˆ— WP e1 {{ Î¦ }} âˆ— wptp t1
-  ==âˆ— âˆƒ e2 t2', t2 = e2 :: t2' âˆ— â–· |==> â—‡ (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/=.
@@ -127,7 +127,7 @@ 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, |==> â–· P) (âˆƒ e2 t2',
-    t2 = e2 :: t2' âˆ— world Ïƒ2 âˆ— WP e2 {{ Î¦ }} âˆ— wptp 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 /=.
   { inversion_clear 1; iIntros "?"; eauto 10. }
@@ -148,8 +148,8 @@ 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, |==> â–· P) (â–  Ï† v2).
+  world Ïƒ1 âˆ— WP e1 {{ v, âŒœÏ† vâŒ }} âˆ— wptp t1 âŠ¢
+  Nat.iter (S (S n)) (Î» P, |==> â–· P) âŒœÏ† v2âŒ.
 Proof.
   intros. rewrite wptp_steps //.
   rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
@@ -159,7 +159,7 @@ Proof.
 Qed.
 
 Lemma wp_safe e Ïƒ Î¦ :
-  world Ïƒ âˆ— WP e {{ Î¦ }} ==âˆ— â–· â–  (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. }
@@ -170,7 +170,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, |==> â–· 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.
@@ -180,9 +180,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, |==> â–· 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.
@@ -196,7 +196,7 @@ Qed.
 End adequacy.
 
 Theorem wp_adequacy Î£ `{irisPreG Î› Î£} e Ïƒ Ï† :
-  (âˆ€ `{irisG Î› Î£}, ownP Ïƒ âŠ¢ WP e {{ v, â–  Ï† v }}) â†’
+  (âˆ€ `{irisG Î› Î£}, ownP Ïƒ âŠ¢ WP e {{ v, âŒœÏ† vâŒ }}) â†’
   adequate e Ïƒ Ï†.
 Proof.
   intros Hwp; split.
@@ -214,7 +214,7 @@ Qed.
 
 Theorem wp_invariance Î£ `{irisPreG Î› Î£} e Ïƒ1 t2 Ïƒ2 I Ï† Î¦ :
   (âˆ€ `{irisG Î› Î£}, ownP Ïƒ1 ={âŠ¤}=âˆ— I âˆ— WP e {{ Î¦ }}) â†’
-  (âˆ€ `{irisG Î› Î£}, I ={âŠ¤,âˆ…}=âˆ— âˆƒ Ïƒ', ownP Ïƒ' âˆ§ â–  Ï† Ïƒ') â†’
+  (âˆ€ `{irisG Î› Î£}, I ={âŠ¤,âˆ…}=âˆ— âˆƒ Ïƒ', ownP Ïƒ' âˆ§ âŒœÏ† Ïƒ'âŒ) â†’
   rtc step ([e], Ïƒ1) (t2, Ïƒ2) â†’
   Ï† Ïƒ2.
 Proof.
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index a35324f53db2e7074b72c877a4ec0af57b6f0ffd..e075f00b74512e03f9b6a48486c29740aece01a8 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -16,8 +16,8 @@ Lemma wp_ectx_bind {E e} K Î¦ :
 Proof. apply: weakestpre.wp_bind. Qed.
 
 Lemma wp_lift_head_step E Î¦ e1 :
-  (|={E,âˆ…}=> âˆƒ Ïƒ1, â–  head_reducible e1 Ïƒ1 âˆ— â–· ownP Ïƒ1 âˆ—
-    â–· âˆ€ e2 Ïƒ2 efs, â–  head_step e1 Ïƒ1 e2 Ïƒ2 efs âˆ— ownP Ïƒ2
+  (|={E,âˆ…}=> âˆƒ Ïƒ1, âŒœhead_reducible e1 Ïƒ1âŒ âˆ— â–· ownP Ïƒ1 âˆ—
+    â–· âˆ€ e2 Ïƒ2 efs, âŒœhead_step e1 Ïƒ1 e2 Ïƒ2 efsâŒ âˆ— ownP Ïƒ2
           ={âˆ…,E}=âˆ— WP e2 @ E {{ Î¦ }} âˆ— [âˆ— list] ef âˆˆ efs, WP ef {{ _, True }})
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
@@ -30,7 +30,7 @@ Qed.
 Lemma wp_lift_pure_head_step E Î¦ e1 :
   (âˆ€ Ïƒ1, head_reducible e1 Ïƒ1) â†’
   (âˆ€ Ïƒ1 e2 Ïƒ2 efs, head_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ Ïƒ1 = Ïƒ2) â†’
-  (â–· âˆ€ e2 efs Ïƒ, â–  head_step e1 Ïƒ e2 Ïƒ efs â†’
+  (â–· âˆ€ e2 efs Ïƒ, âŒœhead_step e1 Ïƒ e2 Ïƒ efsâŒ â†’
     WP e2 @ E {{ Î¦ }} âˆ— [âˆ— list] ef âˆˆ efs, WP ef {{ _, True }})
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
@@ -42,7 +42,7 @@ Lemma wp_lift_atomic_head_step {E Î¦} e1 Ïƒ1 :
   atomic e1 â†’
   head_reducible e1 Ïƒ1 â†’
   â–· ownP Ïƒ1 âˆ— â–· (âˆ€ v2 Ïƒ2 efs,
-  â–  head_step e1 Ïƒ1 (of_val v2) Ïƒ2 efs âˆ§ ownP Ïƒ2 -âˆ—
+  âŒœhead_step e1 Ïƒ1 (of_val v2) Ïƒ2 efsâŒ âˆ§ ownP Ïƒ2 -âˆ—
     Î¦ v2 âˆ— [âˆ— list] ef âˆˆ efs, WP ef {{ _, True }})
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 0f8b104df742cb9e160d8ec4bde0466ccb60865b..8c18831da0a8cf313b986ba48daf53ece7838504 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -56,7 +56,7 @@ Proof. solve_proper. Qed.
 Lemma ht_alt E P Î¦ e : (P âŠ¢ WP e @ E {{ Î¦ }}) â†’ {{ P }} e @ E {{ Î¦ }}.
 Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.
 
-Lemma ht_val E v : {{ True }} of_val v @ E {{ v', v = v' }}.
+Lemma ht_val E v : {{ True }} of_val v @ E {{ v', âŒœv = v'âŒ }}.
 Proof. iIntros "!# _". by iApply wp_value'. Qed.
 
 Lemma ht_vs E P P' Î¦ Î¦' e :
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 4e4f84916a4babc9c3c640b6515e5aae5f1592f3..cac55e4840730cd8580322683392c8a82dd29a1e 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -11,8 +11,8 @@ Implicit Types P Q : iProp Î£.
 Implicit Types Î¦ : val Î› â†’ iProp Î£.
 
 Lemma wp_lift_step E Î¦ e1 :
-  (|={E,âˆ…}=> âˆƒ Ïƒ1, â–  reducible e1 Ïƒ1 âˆ— â–· ownP Ïƒ1 âˆ—
-    â–· âˆ€ e2 Ïƒ2 efs, â–  prim_step e1 Ïƒ1 e2 Ïƒ2 efs âˆ— ownP Ïƒ2
+  (|={E,âˆ…}=> âˆƒ Ïƒ1, âŒœreducible e1 Ïƒ1âŒ âˆ— â–· ownP Ïƒ1 âˆ—
+    â–· âˆ€ e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 e2 Ïƒ2 efsâŒ âˆ— ownP Ïƒ2
           ={âˆ…,E}=âˆ— WP e2 @ E {{ Î¦ }} âˆ— [âˆ— list] ef âˆˆ efs, WP ef {{ _, True }})
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
@@ -31,7 +31,7 @@ Qed.
 Lemma wp_lift_pure_step `{Inhabited (state Î›)} E Î¦ e1 :
   (âˆ€ Ïƒ1, reducible e1 Ïƒ1) â†’
   (âˆ€ Ïƒ1 e2 Ïƒ2 efs, prim_step e1 Ïƒ1 e2 Ïƒ2 efs â†’ Ïƒ1 = Ïƒ2) â†’
-  (â–· âˆ€ e2 efs Ïƒ, â–  prim_step e1 Ïƒ e2 Ïƒ efs â†’
+  (â–· âˆ€ e2 efs Ïƒ, âŒœprim_step e1 Ïƒ e2 Ïƒ efsâŒ â†’
     WP e2 @ E {{ Î¦ }} âˆ— [âˆ— list] ef âˆˆ efs, WP ef {{ _, True }})
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
@@ -47,7 +47,7 @@ Qed.
 Lemma wp_lift_atomic_step {E Î¦} e1 Ïƒ1 :
   atomic e1 â†’
   reducible e1 Ïƒ1 â†’
-  (â–· ownP Ïƒ1 âˆ— â–· âˆ€ v2 Ïƒ2 efs, â–  prim_step e1 Ïƒ1 (of_val v2) Ïƒ2 efs âˆ— ownP Ïƒ2 -âˆ—
+  (â–· ownP Ïƒ1 âˆ— â–· âˆ€ v2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 (of_val v2) Ïƒ2 efsâŒ âˆ— ownP Ïƒ2 -âˆ—
     Î¦ v2 âˆ— [âˆ— list] ef âˆˆ efs, WP ef {{ _, True }})
   âŠ¢ WP e1 @ E {{ Î¦ }}.
 Proof.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 5e665c9282b505b8d0bbc14c6f8a22d036d8ee54..cac72d01bb2e7004d3a3404b853db3ae7efb3aa5 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -26,11 +26,11 @@ Definition wp_pre `{irisG Î› Î£}
     (wp : coPset -c> expr Î› -c> (val Î› -c> iProp Î£) -c> iProp Î£) :
     coPset -c> expr Î› -c> (val Î› -c> iProp Î£) -c> iProp Î£ := Î» E e1 Î¦, (
   (* value case *)
-  (âˆƒ v, to_val e1 = Some v âˆ§ |={E}=> Î¦ v) âˆ¨
+  (âˆƒ v, âŒœto_val e1 = Some vâŒ âˆ§ |={E}=> Î¦ v) âˆ¨
   (* step case *)
-  (to_val e1 = None âˆ§ âˆ€ Ïƒ1,
-     ownP_auth Ïƒ1 ={E,âˆ…}=âˆ— â–  reducible e1 Ïƒ1 âˆ—
-     â–· âˆ€ e2 Ïƒ2 efs, â–  prim_step e1 Ïƒ1 e2 Ïƒ2 efs ={âˆ…,E}=âˆ—
+  (âŒœto_val e1 = NoneâŒ âˆ§ âˆ€ Ïƒ1,
+     ownP_auth Ïƒ1 ={E,âˆ…}=âˆ— âŒœreducible e1 Ïƒ1âŒ âˆ—
+     â–· âˆ€ e2 Ïƒ2 efs, âŒœprim_step e1 Ïƒ1 e2 Ïƒ2 efsâŒ ={âˆ…,E}=âˆ—
        ownP_auth Ïƒ2 âˆ— wp E e2 Î¦ âˆ—
        [âˆ— list] ef âˆˆ efs, wp âŠ¤ ef (Î» _, True)))%I.
 
@@ -119,7 +119,7 @@ Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
 Global Instance ownP_timeless Ïƒ : TimelessP (@ownP (state Î›) Î£ _ Ïƒ).
 Proof. rewrite /ownP; apply _. Qed.
 
-Lemma ownP_agree Ïƒ1 Ïƒ2 : ownP_auth Ïƒ1 âˆ— ownP Ïƒ2 âŠ¢ Ïƒ1 = Ïƒ2.
+Lemma ownP_agree Ïƒ1 Ïƒ2 : ownP_auth Ïƒ1 âˆ— ownP Ïƒ2 âŠ¢ âŒœÏƒ1 = Ïƒ2âŒ.
 Proof.
   rewrite /ownP /ownP_auth -own_op own_valid -auth_both_op.
   by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index e184e233ff1b26ba8585f16608d6e5d3f2842720..5edcb5d02a6c483c55d385bae46f1b4000f67ffa 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -21,7 +21,7 @@ Global Instance from_assumption_bupd p P Q :
 Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
 
 (* IntoPure *)
-Global Instance into_pure_pure Ï† : @IntoPure M (â–  Ï†) Ï†.
+Global Instance into_pure_pure Ï† : @IntoPure M âŒœÏ†âŒ Ï†.
 Proof. done. Qed.
 Global Instance into_pure_eq {A : ofeT} (a b : A) :
   Timeless a â†’ @IntoPure M (a â‰¡ b) (a â‰¡ b).
@@ -31,7 +31,7 @@ Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
 (* FromPure *)
-Global Instance from_pure_pure Ï† : @FromPure M (â–  Ï†) Ï†.
+Global Instance from_pure_pure Ï† : @FromPure M âŒœÏ†âŒ Ï†.
 Proof. done. Qed.
 Global Instance from_pure_internal_eq {A : ofeT} (a b : A) :
   @FromPure M (a â‰¡ b) (a â‰¡ b).
@@ -240,7 +240,7 @@ Qed.
 (* Frame *)
 Global Instance frame_here R : Frame R R True.
 Proof. by rewrite /Frame right_id. Qed.
-Global Instance frame_here_pure Ï† Q : FromPure Q Ï† â†’ Frame (â–  Ï†) Q True.
+Global Instance frame_here_pure Ï† Q : FromPure Q Ï† â†’ Frame âŒœÏ†âŒ Q True.
 Proof. rewrite /FromPure /Frame=> ->. by rewrite right_id. Qed.
 
 Class MakeSep (P Q PQ : uPred M) := make_sep : P âˆ— Q âŠ£âŠ¢ PQ.
diff --git a/proofmode/classes.v b/proofmode/classes.v
index c17d464bee33ba18d7d2a407057cee8c07b7529a..c9b0bccb9cc92daaf86fcf07ba838d5edf7e527b 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -8,10 +8,10 @@ Implicit Types P Q : uPred M.
 Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : â–¡?p P âŠ¢ Q.
 Global Arguments from_assumption _ _ _ {_}.
 
-Class IntoPure (P : uPred M) (Ï† : Prop) := into_pure : P âŠ¢ â–  Ï†.
+Class IntoPure (P : uPred M) (Ï† : Prop) := into_pure : P âŠ¢ âŒœÏ†âŒ.
 Global Arguments into_pure : clear implicits.
 
-Class FromPure (P : uPred M) (Ï† : Prop) := from_pure : â–  Ï† âŠ¢ P.
+Class FromPure (P : uPred M) (Ï† : Prop) := from_pure : âŒœÏ†âŒ âŠ¢ P.
 Global Arguments from_pure : clear implicits.
 
 Class IntoPersistentP (P Q : uPred M) := into_persistentP : P âŠ¢ â–¡ Q.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 234fa9086b9f79c84657371fe43d96988b56d0e4..5fef411c249465694f2e9e2d160b4feca67ad15e 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -19,7 +19,7 @@ Record envs_wf {M} (Î” : envs M) := {
 }.
 
 Coercion of_envs {M} (Î” : envs M) : uPred M :=
-  (â–  envs_wf Î” âˆ— â–¡ [âˆ—] env_persistent Î” âˆ— [âˆ—] env_spatial Î”)%I.
+  (âŒœenvs_wf Î”âŒ âˆ— â–¡ [âˆ—] env_persistent Î” âˆ— [âˆ—] env_spatial Î”)%I.
 Instance: Params (@of_envs) 1.
 
 Record envs_Forall2 {M} (R : relation (uPred M)) (Î”1 Î”2 : envs M) : Prop := {
@@ -110,7 +110,7 @@ Implicit Types Î” : envs M.
 Implicit Types P Q : uPred M.
 
 Lemma of_envs_def Î” :
-  of_envs Î” = (â–  envs_wf Î” âˆ— â–¡ [âˆ—] env_persistent Î” âˆ— [âˆ—] env_spatial Î”)%I.
+  of_envs Î” = (âŒœenvs_wf Î”âŒ âˆ— â–¡ [âˆ—] env_persistent Î” âˆ— [âˆ—] env_spatial Î”)%I.
 Proof. done. Qed.
 
 Lemma envs_lookup_delete_Some Î” Î”' i p P :
@@ -397,7 +397,7 @@ Proof.
   rewrite (into_pure P); by apply pure_elim_sep_l.
 Qed.
 
-Lemma tac_pure_revert Î” Ï† Q : (Î” âŠ¢ â–  Ï† â†’ Q) â†’ (Ï† â†’ Î” âŠ¢ Q).
+Lemma tac_pure_revert Î” Ï† Q : (Î” âŠ¢ âŒœÏ†âŒ â†’ Q) â†’ (Ï† â†’ Î” âŠ¢ Q).
 Proof. intros HÎ” ?. by rewrite HÎ” pure_True // left_id. Qed.
 
 (** * Later *)
@@ -476,7 +476,7 @@ Proof.
   by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
 Qed.
 Lemma tac_pure_impl_intro Î” (Ï† Ïˆ : Prop) :
-  (Ï† â†’ Î” âŠ¢ â–  Ïˆ) â†’ Î” âŠ¢ â–  (Ï† â†’ Ïˆ).
+  (Ï† â†’ Î” âŠ¢ âŒœÏˆâŒ) â†’ Î” âŠ¢ âŒœÏ† â†’ ÏˆâŒ.
 Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
 Lemma tac_impl_intro_pure Î” P Ï† Q : IntoPure P Ï† â†’ (Ï† â†’ Î” âŠ¢ Q) â†’ Î” âŠ¢ P â†’ Q.
 Proof.
@@ -744,8 +744,8 @@ Qed.
 
 (** * Framing *)
 Lemma tac_frame_pure Î” (Ï† : Prop) P Q :
-  Ï† â†’ Frame (â–  Ï†) P Q â†’ (Î” âŠ¢ Q) â†’ Î” âŠ¢ P.
-Proof. intros ?? ->. by rewrite -(frame (â–  Ï†) P) pure_True // left_id. Qed.
+  Ï† â†’ Frame âŒœÏ†âŒ P Q â†’ (Î” âŠ¢ Q) â†’ Î” âŠ¢ P.
+Proof. intros ?? ->. by rewrite -(frame âŒœÏ†âŒ P) pure_True // left_id. Qed.
 
 Lemma tac_frame Î” Î”' i p R P Q :
   envs_lookup_delete i Î” = Some (p, R, Î”') â†’ Frame R P Q â†’
@@ -781,7 +781,7 @@ Lemma tac_forall_intro {A} Î” (Î¦ : A â†’ uPred M) : (âˆ€ a, Î” âŠ¢ Î¦ a) â†’ Î”
 Proof. apply forall_intro. Qed.
 
 Lemma tac_pure_forall_intro {A} Î” (Ï† : A â†’ Prop) :
-  (âˆ€ a, Î” âŠ¢ â–  Ï† a) â†’ Î” âŠ¢ â–  âˆ€ a, Ï† a.
+  (âˆ€ a, Î” âŠ¢ âŒœÏ† aâŒ) â†’ Î” âŠ¢ âŒœâˆ€ a, Ï† aâŒ.
 Proof. intros. rewrite pure_forall. by apply forall_intro. Qed.
 
 Class ForallSpecialize {As} (xs : hlist As)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 831e049dd5b7cf5ca6449d9dcc6becb1ed3cf9ad..00c6b395a5ee5627aeb3a50cf79d2702a1c15e4e 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -1148,7 +1148,7 @@ Tactic Notation "iRewrite" "-" open_constr(lem) "in" constr(H) :=
   iRewriteCore true lem in H.
 
 Ltac iSimplifyEq := repeat (
-  iMatchGoal ltac:(fun H P => match P with (_ = _)%I => iDestruct H as %? end)
+  iMatchGoal ltac:(fun H P => match P with (âŒœ_ = _âŒ)%I => iDestruct H as %? end)
   || simplify_eq/=).
 
 (** * Update modality *)
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index a4b7e564d5d291461cd37d232a4fd8d3894cdb0e..6b60585dc9f43e65c0640038cd9185781543c2ed 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -17,7 +17,7 @@ Section client.
   Context `{!heapG Î£, !barrierG Î£, !spawnG Î£} (N : namespace).
 
   Definition y_inv (q : Qp) (l : loc) : iProp Î£ :=
-    (âˆƒ f : val, l â†¦{q} f âˆ— â–¡ âˆ€ n : Z, WP f #n {{ v, v = #(n + 42) }})%I.
+    (âˆƒ f : val, l â†¦{q} f âˆ— â–¡ âˆ€ n : Z, WP f #n {{ v, âŒœv = #(n + 42)âŒ }})%I.
 
   Lemma y_inv_split q l : y_inv q l âŠ¢ (y_inv (q/2) l âˆ— y_inv (q/2) l).
   Proof.
diff --git a/tests/counter.v b/tests/counter.v
index 053a5b7ba48c395bbf6a38ed204c6996f226b59b..9bc8d14b9a54f82eaffde6ea6c98516ef64dbbd8 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -85,7 +85,7 @@ Definition I (Î³ : gname) (l : loc) : iProp Î£ :=
   (âˆƒ c : nat, l â†¦ #c âˆ— own Î³ (Auth c))%I.
 
 Definition C (l : loc) (n : nat) : iProp Î£ :=
-  (âˆƒ N Î³, heapN âŠ¥ N âˆ§ heap_ctx âˆ§ inv N (I Î³ l) âˆ§ own Î³ (Frag n))%I.
+  (âˆƒ N Î³, âŒœheapN âŠ¥ NâŒ âˆ§ heap_ctx âˆ§ inv N (I Î³ l) âˆ§ own Î³ (Frag n))%I.
 
 (** The main proofs. *)
 Global Instance C_persistent l n : PersistentP (C l n).
@@ -93,7 +93,7 @@ Proof. apply _. Qed.
 
 Lemma newcounter_spec N :
   heapN âŠ¥ N â†’
-  heap_ctx âŠ¢ {{ True }} newcounter #() {{ v, âˆƒ l, v = #l âˆ§ C l 0 }}.
+  heap_ctx âŠ¢ {{ True }} newcounter #() {{ v, âˆƒ l, âŒœv = #lâŒ âˆ§ C l 0 }}.
 Proof.
   iIntros (?) "#Hh !# _ /=". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl".
   iMod (own_alloc (Auth 0)) as (Î³) "HÎ³"; first done.
@@ -104,7 +104,7 @@ Proof.
 Qed.
 
 Lemma incr_spec l n :
-  {{ C l n }} incr #l {{ v, v = #() âˆ§ C l (S n) }}.
+  {{ C l n }} incr #l {{ v, âŒœv = #()âŒ âˆ§ C l (S n) }}.
 Proof.
   iIntros "!# Hl /=". iLÃ¶b as "IH". wp_rec.
   iDestruct "Hl" as (N Î³) "(% & #Hh & #Hinv & HÎ³f)".
@@ -126,7 +126,7 @@ Proof.
 Qed.
 
 Lemma read_spec l n :
-  {{ C l n }} read #l {{ v, âˆƒ m : nat, â–  (v = #m âˆ§ n â‰¤ m) âˆ§ C l m }}.
+  {{ C l n }} read #l {{ v, âˆƒ m : nat, âŒœv = #m âˆ§ n â‰¤ mâŒ âˆ§ C l m }}.
 Proof.
   iIntros "!# Hl /=". iDestruct "Hl" as (N Î³) "(% & #Hh & #Hinv & HÎ³f)".
   rewrite /read /=. wp_let. iInv N as (c) "[Hl HÎ³]" "Hclose". wp_load.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 4cd2dd065c4d698c85de78cea753d0904c4db8fa..3f6f8c7fef2bd7525268dc8502952804016cbbfc 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -12,7 +12,7 @@ Section LiftingTests.
   Definition heap_e  : expr :=
     let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
   Lemma heap_e_spec E :
-     nclose heapN âŠ† E â†’ heap_ctx âŠ¢ WP heap_e @ E {{ v, v = #2 }}.
+     nclose heapN âŠ† E â†’ heap_ctx âŠ¢ WP heap_e @ E {{ v, âŒœv = #2âŒ }}.
   Proof.
     iIntros (HN) "#?". rewrite /heap_e.
     wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
@@ -23,7 +23,7 @@ Section LiftingTests.
     let: "y" := ref #1 in
     "x" <- !"x" + #1 ;; !"x".
   Lemma heap_e2_spec E :
-     nclose heapN âŠ† E â†’ heap_ctx âŠ¢ WP heap_e2 @ E {{ v, v = #2 }}.
+     nclose heapN âŠ† E â†’ heap_ctx âŠ¢ WP heap_e2 @ E {{ v, âŒœv = #2âŒ }}.
   Proof.
     iIntros (HN) "#?". rewrite /heap_e2.
     wp_alloc l. wp_let. wp_alloc l'. wp_let.
@@ -59,7 +59,7 @@ Section LiftingTests.
   Qed.
 
   Lemma Pred_user E :
-    True âŠ¢ WP let: "x" := Pred #42 in Pred "x" @ E {{ v, v = #40 }}.
+    True âŠ¢ WP let: "x" := Pred #42 in Pred "x" @ E {{ v, âŒœv = #40âŒ }}.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 5af0d7fab958603044af441939d79362c606aeef..64565e93fa8e9047cf8fe087829c52ed5851227c 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -10,8 +10,8 @@ Implicit Types l : loc.
 
 Fixpoint is_list (hd : val) (xs : list val) : iProp Î£ :=
   match xs with
-  | [] => hd = NONEV
-  | x :: xs => âˆƒ l hd', hd = SOMEV #l âˆ— l â†¦ (x,hd') âˆ— is_list hd' xs
+  | [] => âŒœhd = NONEVâŒ
+  | x :: xs => âˆƒ l hd', âŒœhd = SOMEV #lâŒ âˆ— l â†¦ (x,hd') âˆ— is_list hd' xs
   end%I.
 
 Definition rev : val :=
diff --git a/tests/one_shot.v b/tests/one_shot.v
index aa97d00877c7167919a90d0de650db3000fdd044..04c0354c25c0dd4cbb80bd02e53500108dabba7e 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -37,7 +37,7 @@ Definition one_shot_inv (Î³ : gname) (l : loc) : iProp Î£ :=
 
 Lemma wp_one_shot (Î¦ : val â†’ iProp Î£) :
   heap_ctx âˆ— (âˆ€ f1 f2 : val,
-    (âˆ€ n : Z, â–¡ WP f1 #n {{ w, w = #true âˆ¨ w = #false }}) âˆ—
+    (âˆ€ n : Z, â–¡ WP f1 #n {{ w, âŒœw = #trueâŒ âˆ¨ âŒœw = #falseâŒ }}) âˆ—
     â–¡ WP f2 #() {{ g, â–¡ WP g #() {{ _, True }} }} -âˆ— Î¦ (f1,f2)%V)
   âŠ¢ WP one_shot_example #() {{ Î¦ }}.
 Proof.
@@ -57,14 +57,14 @@ Proof.
       rewrite /one_shot_inv; eauto 10.
   - iIntros "!#". wp_seq. wp_bind (! _)%E.
     iInv N as ">HÎ³" "Hclose".
-    iAssert (âˆƒ v, l â†¦ v âˆ— ((v = NONEV âˆ— own Î³ Pending) âˆ¨
-       âˆƒ n : Z, v = SOMEV #n âˆ— own Î³ (Shot n)))%I with "[HÎ³]" as "Hv".
+    iAssert (âˆƒ v, l â†¦ v âˆ— ((âŒœv = NONEVâŒ âˆ— own Î³ Pending) âˆ¨
+       âˆƒ n : Z, âŒœv = SOMEV #nâŒ âˆ— own Î³ (Shot n)))%I with "[HÎ³]" as "Hv".
     { iDestruct "HÎ³" as "[[Hl HÎ³]|Hl]"; last iDestruct "Hl" as (m) "[Hl HÎ³]".
       + iExists NONEV. iFrame. eauto.
       + iExists (SOMEV #m). iFrame. eauto. }
     iDestruct "Hv" as (v) "[Hl Hv]". wp_load.
-    iAssert (one_shot_inv Î³ l âˆ— (v = NONEV âˆ¨ âˆƒ n : Z,
-      v = SOMEV #n âˆ— own Î³ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
+    iAssert (one_shot_inv Î³ l âˆ— (âŒœv = NONEVâŒ âˆ¨ âˆƒ n : Z,
+      âŒœv = SOMEV #nâŒ âˆ— own Î³ (Shot n)))%I with "[Hl Hv]" as "[Hinv #Hv]".
     { iDestruct "Hv" as "[[% ?]|Hv]"; last iDestruct "Hv" as (m) "[% ?]"; subst.
       + iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
@@ -86,7 +86,7 @@ Qed.
 Lemma ht_one_shot (Î¦ : val â†’ iProp Î£) :
   heap_ctx âŠ¢ {{ True }} one_shot_example #()
     {{ ff,
-      (âˆ€ n : Z, {{ True }} Fst ff #n {{ w, w = #true âˆ¨ w = #false }}) âˆ—
+      (âˆ€ n : Z, {{ True }} Fst ff #n {{ w, âŒœw = #trueâŒ âˆ¨ âŒœw = #falseâŒ }}) âˆ—
       {{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
     }}.
 Proof.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 97bec6d8bde135a52fb75557725bd0e9086d2a8e..ab97cc55d2f2881e54f3c06830b98a33f72e6f7f 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Import invariants.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
-  â–¡ (P âˆ¨ Q) âŠ¢ (âˆ€ x, x = 0 âˆ¨ x = 1) â†’ (Q âˆ¨ P).
+  â–¡ (P âˆ¨ Q) âŠ¢ (âˆ€ x, âŒœx = 0âŒ âˆ¨ âŒœx = 1âŒ) â†’ (Q âˆ¨ P).
 Proof.
   iIntros "#H #H2".
   (* should remove the disjunction "H" *)
@@ -17,8 +17,8 @@ Lemma demo_1 (M : ucmraT) (P1 P2 P3 : nat â†’ uPred M) :
     â–¡ (uPred_ownM (a â‹… b) -âˆ—
     (âˆƒ y1 y2 c, P1 ((x + y1) + y2) âˆ§ True âˆ§ â–¡ uPred_ownM c) -âˆ—
     â–¡ â–· (âˆ€ z, P2 z âˆ¨ True â†’ P2 z) -âˆ—
-    â–· (âˆ€ n m : nat, P1 n â†’ â–¡ ((True âˆ§ P2 n) â†’ â–¡ (n = n â†” P3 n))) -âˆ—
-    â–· (x = 0) âˆ¨ âˆƒ x z, â–· P3 (x + z) âˆ— uPred_ownM b âˆ— uPred_ownM (core b)).
+    â–· (âˆ€ n m : nat, P1 n â†’ â–¡ ((True âˆ§ P2 n) â†’ â–¡ (âŒœn = nâŒ â†” P3 n))) -âˆ—
+    â–· âŒœx = 0âŒ âˆ¨ âˆƒ x z, â–· P3 (x + z) âˆ— uPred_ownM b âˆ— uPred_ownM (core b)).
 Proof.
   iIntros (i [|j] a b ?) "!# [Ha Hb] H1 #H2 H3"; setoid_subst.
   { iLeft. by iNext. }
@@ -38,7 +38,7 @@ Qed.
 
 Lemma demo_2 (M : ucmraT) (P1 P2 P3 P4 Q : uPred M) (P5 : nat â†’ uPredC M):
     P2 âˆ— (P3 âˆ— Q) âˆ— True âˆ— P1 âˆ— P2 âˆ— (P4 âˆ— (âˆƒ x:nat, P5 x âˆ¨ P3)) âˆ— True
-  âŠ¢ P1 -âˆ— (True âˆ— True) -âˆ— (((P2 âˆ§ False âˆ¨ P2 âˆ§ 0 = 0) âˆ— P3) âˆ— Q âˆ— P1 âˆ— True) âˆ§
+  âŠ¢ P1 -âˆ— (True âˆ— True) -âˆ— (((P2 âˆ§ False âˆ¨ P2 âˆ§ âŒœ0 = 0âŒ) âˆ— P3) âˆ— Q âˆ— P1 âˆ— True) âˆ§
      (P2 âˆ¨ False) âˆ§ (False â†’ P5 0).
 Proof.
   (* Intro-patterns do something :) *)
@@ -54,7 +54,7 @@ Proof.
 Qed.
 
 Lemma demo_3 (M : ucmraT) (P1 P2 P3 : uPred M) :
-  P1 âˆ— P2 âˆ— P3 âŠ¢ â–· P1 âˆ— â–· (P2 âˆ— âˆƒ x, (P3 âˆ§ x = 0) âˆ¨ P3).
+  P1 âˆ— P2 âˆ— P3 âŠ¢ â–· P1 âˆ— â–· (P2 âˆ— âˆƒ x, (P3 âˆ§ âŒœx = 0âŒ) âˆ¨ P3).
 Proof. iIntros "($ & $ & H)". iFrame "H". iNext. by iExists 0. Qed.
 
 Definition foo {M} (P : uPred M) := (P â†’ P)%I.
@@ -74,7 +74,7 @@ Qed.
 
 Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
   True âŠ¢ âˆ€ x y z : nat,
-    x = plus 0 x â†’ y = 0 â†’ z = 0 â†’ P â†’ â–¡ Q â†’ foo (x â‰¡ x).
+    âŒœx = plus 0 xâŒ â†’ âŒœy = 0âŒ â†’ âŒœz = 0âŒ â†’ P â†’ â–¡ Q â†’ foo (x â‰¡ x).
 Proof.
   iIntros (a) "*".
   iIntros "#Hfoo **".
@@ -102,5 +102,5 @@ Section iris.
 End iris.
 
 Lemma demo_9 (M : ucmraT) (x y z : M) :
-  âœ“ x â†’ â–  (y â‰¡ z) âŠ¢ (âœ“ x âˆ§ âœ“ x âˆ§ y â‰¡ z : uPred M).
+  âœ“ x â†’ âŒœy â‰¡ zâŒ âŠ¢ (âœ“ x âˆ§ âœ“ x âˆ§ y â‰¡ z : uPred M).
 Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index ff0978afdc3a9bed68ad9ae2b1e10050f47436bb..8e3b9b9c4fabc88f574429062169fb5135f65376 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -9,10 +9,10 @@ Inductive tree :=
 
 Fixpoint is_tree `{!heapG Î£} (v : val) (t : tree) : iProp Î£ :=
   match t with
-  | leaf n => v = InjLV #n
+  | leaf n => âŒœv = InjLV #nâŒ
   | node tl tr =>
      âˆƒ (ll lr : loc) (vl vr : val),
-       v = InjRV (#ll,#lr) âˆ— ll â†¦ vl âˆ— is_tree vl tl âˆ— lr â†¦ vr âˆ— is_tree vr tr
+       âŒœv = InjRV (#ll,#lr)âŒ âˆ— ll â†¦ vl âˆ— is_tree vl tl âˆ— lr â†¦ vr âˆ— is_tree vr tr
   end%I.
 
 Fixpoint sum (t : tree) : Z :=