diff --git a/base_logic/lib/auth.v b/base_logic/lib/auth.v
index 30054193777ee2356abffd6e09498ff36b177dbb..4c4647a570f7c7cbd50a2c0994262b0abb8d6dce 100644
--- a/base_logic/lib/auth.v
+++ b/base_logic/lib/auth.v
@@ -128,10 +128,10 @@ Section auth.
   Qed.
 
   Lemma auth_open E N Î³ a :
-    nclose N âŠ† E â†’
-    auth_ctx Î³ N f Ï† âˆ— auth_own Î³ a ={E,Eâˆ–N}=âˆ— âˆƒ t,
+    â†‘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.
+      âŒœ(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 cd2f1f8fc336fd54dfde1e83003e418c0501947d..1343d4a4e7103fa92ce3a24925e57f6ea7d99a19 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -105,7 +105,7 @@ Proof.
 Qed.
 
 Lemma box_delete E f P Q Î³ :
-  nclose N âŠ† E â†’
+  â†‘N âŠ† E â†’
   f !! Î³ = Some false â†’
   slice N Î³ Q âˆ— â–· box N f P ={E}=âˆ— âˆƒ P',
     â–· â–· (P â‰¡ (Q âˆ— P')) âˆ— â–· box N (delete Î³ f) P'.
@@ -125,7 +125,7 @@ Proof.
 Qed.
 
 Lemma box_fill E f Î³ P Q :
-  nclose N âŠ† E â†’
+  â†‘N âŠ† E â†’
   f !! Î³ = Some false â†’
   slice N Î³ Q âˆ— â–· Q âˆ— â–· box N f P ={E}=âˆ— â–· box N (<[Î³:=true]> f) P.
 Proof.
@@ -144,7 +144,7 @@ Proof.
 Qed.
 
 Lemma box_empty E f P Q Î³ :
-  nclose N âŠ† E â†’
+  â†‘N âŠ† E â†’
   f !! Î³ = Some true â†’
   slice N Î³ Q âˆ— â–· box N f P ={E}=âˆ— â–· Q âˆ— â–· box N (<[Î³:=false]> f) P.
 Proof.
@@ -164,7 +164,7 @@ Proof.
 Qed.
 
 Lemma box_fill_all E f P :
-  nclose N âŠ† E â†’
+  â†‘N âŠ† E â†’
   box N f P âˆ— â–· P ={E}=âˆ— box N (const true <$> f) P.
 Proof.
   iIntros (?) "[H HP]"; iDestruct "H" as (Î¦) "[#HeqP Hf]".
@@ -181,7 +181,7 @@ Proof.
 Qed.
 
 Lemma box_empty_all E f P :
-  nclose N âŠ† E â†’
+  â†‘N âŠ† E â†’
   map_Forall (Î» _, (true =)) f â†’
   box N f P ={E}=âˆ— â–· P âˆ— box N (const false <$> f) P.
 Proof.
diff --git a/base_logic/lib/cancelable_invariants.v b/base_logic/lib/cancelable_invariants.v
index e4231ef1657b8cb8f710e3d278d272ff1e8e3fed..35717dfb20aa22452f2a54b15196587323ea88fc 100644
--- a/base_logic/lib/cancelable_invariants.v
+++ b/base_logic/lib/cancelable_invariants.v
@@ -51,8 +51,7 @@ Section proofs.
     iMod (inv_alloc N _ (P âˆ¨ own Î³ 1%Qp)%I with "[HP]"); eauto.
   Qed.
 
-  Lemma cinv_cancel E N Î³ P :
-    nclose N âŠ† E â†’ cinv N Î³ P âŠ¢ cinv_own Î³ 1 ={E}=âˆ— â–· P.
+  Lemma cinv_cancel E N Î³ P : â†‘N âŠ† E â†’ cinv N Î³ P âŠ¢ cinv_own Î³ 1 ={E}=âˆ— â–· P.
   Proof.
     rewrite /cinv. iIntros (?) "#Hinv HÎ³".
     iInv N as "[$|>HÎ³']" "Hclose"; first iApply "Hclose"; eauto.
@@ -60,8 +59,8 @@ Section proofs.
   Qed.
 
   Lemma cinv_open E N Î³ p P :
-    nclose N âŠ† E â†’
-    cinv N Î³ P âŠ¢ cinv_own Î³ p ={E,Eâˆ–N}=âˆ— â–· P âˆ— cinv_own Î³ p âˆ— (â–· P ={Eâˆ–N,E}=âˆ— True).
+    â†‘N âŠ† E â†’
+    cinv N Î³ P âŠ¢ cinv_own Î³ p ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— cinv_own Î³ p âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True).
   Proof.
     rewrite /cinv. iIntros (?) "#Hinv HÎ³".
     iInv N as "[$|>HÎ³']" "Hclose".
diff --git a/base_logic/lib/invariants.v b/base_logic/lib/invariants.v
index 14e4fff3123d852eeabc03428f71acab1a487c63..8e0b12ef4fa68f1a290c37892c400d3dd24ea7ff 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 âˆˆ â†‘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.
@@ -30,8 +30,8 @@ Proof. rewrite inv_eq /inv; apply _. Qed.
 Lemma inv_alloc N E P : â–· P ={E}=âˆ— inv N P.
 Proof.
   rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
-  iMod (ownI_alloc (âˆˆ nclose N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
-  - intros Ef. exists (coPpick (nclose N âˆ– coPset.of_gset Ef)).
+  iMod (ownI_alloc (âˆˆ â†‘ N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
+  - intros Ef. exists (coPpick (â†‘ N âˆ– coPset.of_gset Ef)).
     rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
     apply coPpick_elem_of=> Hfin.
     eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
@@ -41,19 +41,19 @@ Proof.
 Qed.
 
 Lemma inv_open E N P :
-  nclose N âŠ† E â†’ inv N P ={E,Eâˆ–N}=âˆ— â–· P âˆ— (â–· P ={Eâˆ–N,E}=âˆ— True).
+  â†‘N âŠ† E â†’ inv N P ={E,Eâˆ–â†‘N}=âˆ— â–· P âˆ— (â–· P ={Eâˆ–â†‘N,E}=âˆ— True).
 Proof.
   rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
   iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
-  rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver.
-  rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver.
+  rewrite {1 4}(union_difference_L (â†‘ N) E) // ownE_op; last set_solver.
+  rewrite {1 5}(union_difference_L {[ i ]} (â†‘ N)) // ownE_op; last set_solver.
   iIntros "(Hw & [HE $] & $) !> !>".
   iDestruct (ownI_open i P with "[$Hw $HE $HiP]") as "($ & $ & HD)".
   iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame.
 Qed.
 
 Lemma inv_open_timeless E N P `{!TimelessP P} :
-  nclose N âŠ† E â†’ inv N P ={E,Eâˆ–N}=âˆ— P âˆ— (P ={Eâˆ–N,E}=âˆ— True).
+  â†‘N âŠ† E â†’ inv N P ={E,Eâˆ–â†‘N}=âˆ— P âˆ— (P ={Eâˆ–â†‘N,E}=âˆ— True).
 Proof.
   iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
   iIntros "!> {$HP} HP". iApply "Hclose"; auto.
diff --git a/base_logic/lib/namespaces.v b/base_logic/lib/namespaces.v
index 9bf4bd1c5a81621ae6806cce2693a4053f18ce5e..9798e49afd7be095c277babaf860ae3c139c52b8 100644
--- a/base_logic/lib/namespaces.v
+++ b/base_logic/lib/namespaces.v
@@ -16,7 +16,7 @@ Definition ndot_eq : @ndot = @ndot_def := proj2_sig ndot_aux.
 
 Definition nclose_def (N : namespace) : coPset := coPset_suffixes (encode N).
 Definition nclose_aux : { x | x = @nclose_def }. by eexists. Qed.
-Coercion nclose := proj1_sig nclose_aux.
+Instance nclose : UpClose namespace coPset := proj1_sig nclose_aux.
 Definition nclose_eq : @nclose = @nclose_def := proj2_sig nclose_aux.
 
 Infix ".@" := ndot (at level 19, left associativity) : C_scope.
@@ -27,31 +27,34 @@ Instance ndisjoint : Disjoint namespace := Î» N1 N2, nclose N1 âŠ¥ nclose N2.
 Section namespace.
   Context `{Countable A}.
   Implicit Types x y : A.
+  Implicit Types N : namespace.
+  Implicit Types E : coPset.
 
   Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
   Proof. intros N1 x1 N2 x2; rewrite !ndot_eq=> ?; by simplify_eq. Qed.
 
-  Lemma nclose_nroot : nclose nroot = âŠ¤.
+  Lemma nclose_nroot : â†‘nroot = âŠ¤.
   Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
-  Lemma encode_nclose N : encode N âˆˆ nclose N.
+  Lemma encode_nclose N : encode N âˆˆ â†‘N.
   Proof.
     rewrite nclose_eq.
     by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _).
   Qed.
 
-  Lemma nclose_subseteq N x : nclose (N .@ x) âŠ† nclose N.
+  Lemma nclose_subseteq N x : â†‘N .@ x âŠ† (â†‘N : coPset).
   Proof.
     intros p; rewrite nclose_eq /nclose !ndot_eq !elem_coPset_suffixes.
     intros [q ->]. destruct (list_encode_suffix N (ndot_def N x)) as [q' ?].
     { by exists [encode x]. }
     by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
   Qed.
-  Lemma nclose_subseteq' E N x : nclose N âŠ† E â†’ nclose (N .@ x) âŠ† E.
+
+  Lemma nclose_subseteq' E N x : â†‘N âŠ† E â†’ â†‘N .@ x âŠ† E.
   Proof. intros. etrans; eauto using nclose_subseteq. Qed.
 
-  Lemma ndot_nclose N x : encode (N .@ x) âˆˆ nclose N.
+  Lemma ndot_nclose N x : encode (N .@ x) âˆˆ â†‘ N.
   Proof. apply nclose_subseteq with x, encode_nclose. Qed.
-  Lemma nclose_infinite N : Â¬set_finite (nclose N).
+  Lemma nclose_infinite N : Â¬set_finite (â†‘ N : coPset).
   Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
 
   Lemma ndot_ne_disjoint N x y : x â‰  y â†’ N .@ x âŠ¥ N .@ y.
@@ -61,19 +64,18 @@ Section namespace.
     revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq.
   Qed.
 
-  Lemma ndot_preserve_disjoint_l N E x : nclose N âŠ¥ E â†’ nclose (N .@ x) âŠ¥ E.
+  Lemma ndot_preserve_disjoint_l N E x : â†‘N âŠ¥ E â†’ â†‘N .@ x âŠ¥ E.
   Proof. intros. pose proof (nclose_subseteq N x). set_solver. Qed.
 
-  Lemma ndot_preserve_disjoint_r N E x : E âŠ¥ nclose N â†’ E âŠ¥ nclose (N .@ x).
+  Lemma ndot_preserve_disjoint_r N E x : E âŠ¥ â†‘N â†’ E âŠ¥ â†‘N .@ x.
   Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
 
-  Lemma ndisj_subseteq_difference N E F :
-    E âŠ¥ nclose N â†’ E âŠ† F â†’ E âŠ† F âˆ– nclose N.
+  Lemma ndisj_subseteq_difference N E F : E âŠ¥ â†‘N â†’ E âŠ† F â†’ E âŠ† F âˆ– â†‘N.
   Proof. set_solver. Qed.
 End namespace.
 
 (* The hope is that registering these will suffice to solve most goals
-of the form [N1 âŠ¥ N2] and those of the form [N1 âŠ† E âˆ– N2 âˆ– .. âˆ– Nn]. *)
+of the form [N1 âŠ¥ N2] and those of the form [â†‘N1 âŠ† E âˆ– â†‘N2 âˆ– .. âˆ– â†‘Nn]. *)
 Hint Resolve ndisj_subseteq_difference : ndisj.
 Hint Extern 0 (_ âŠ¥ _) => apply ndot_ne_disjoint; congruence : ndisj.
 Hint Resolve ndot_preserve_disjoint_l : ndisj.
diff --git a/base_logic/lib/sts.v b/base_logic/lib/sts.v
index 15299e9bef424db149d36d7b06d6f14638a342cc..f3f5153a1bd07e1895997f49b303d3f2a97a67a2 100644
--- a/base_logic/lib/sts.v
+++ b/base_logic/lib/sts.v
@@ -117,10 +117,10 @@ Section sts.
   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,
+    â†‘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'.
+      âŒœ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
@@ -135,9 +135,9 @@ Section sts.
   Qed.
 
   Lemma sts_open E N Î³ s0 T :
-    nclose N âŠ† E â†’
-    sts_ctx Î³ N Ï† âˆ— sts_own Î³ s0 T ={E,Eâˆ–N}=âˆ— âˆƒ s,
+    â†‘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.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 c97d31f212753a15bf3c74d536a1d454b0038a72..46f2e3204632c886910c03fb6a0ba1bfa3b254d3 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 âˆˆ â†‘NâŒ âˆ§
           inv tlN (P âˆ— own tid (âˆ…, GSet {[i]}) âˆ¨ tl_own tid {[i]}))%I.
 End defs.
 
@@ -57,8 +57,8 @@ Section proofs.
     iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
     iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
     { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
-      apply (gset_disj_alloc_empty_updateP_strong' (Î» i, i âˆˆ nclose N)).
-      intros Ef. exists (coPpick (nclose N âˆ– coPset.of_gset Ef)).
+      apply (gset_disj_alloc_empty_updateP_strong' (Î» i, i âˆˆ â†‘N)).
+      intros Ef. exists (coPpick (â†‘ N âˆ– coPset.of_gset Ef)).
       rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
       apply coPpick_elem_of=> Hfin.
       eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
@@ -70,14 +70,14 @@ Section proofs.
   Qed.
 
   Lemma tl_inv_open tid tlE E N P :
-    nclose tlN âŠ† tlE â†’ nclose N âŠ† E â†’
-    tl_inv tid N P âŠ¢ tl_own tid E ={tlE}=âˆ— â–· P âˆ— tl_own tid (E âˆ– N) âˆ—
-                       (â–· P âˆ— tl_own tid (E âˆ– N) ={tlE}=âˆ— tl_own tid E).
+    â†‘tlN âŠ† tlE â†’ â†‘N âŠ† E â†’
+    tl_inv tid N P âŠ¢ tl_own tid E ={tlE}=âˆ— â–· P âˆ— tl_own tid (Eâˆ–â†‘N) âˆ—
+                       (â–· P âˆ— tl_own tid (Eâˆ–â†‘N) ={tlE}=âˆ— tl_own tid E).
   Proof.
     rewrite /tl_inv. iIntros (??) "#Htlinv Htoks".
     iDestruct "Htlinv" as (i) "[% Hinv]".
-    rewrite {1 4}(union_difference_L (nclose N) E) //.
-    rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_own_union; [|set_solver..].
+    rewrite {1 4}(union_difference_L (â†‘N) E) //.
+    rewrite {1 5}(union_difference_L {[i]} (â†‘N)) ?tl_own_union; [|set_solver..].
     iDestruct "Htoks" as "[[Htoki $] $]".
     iInv tlN as "[[$ >Hdis]|>Htoki2]" "Hclose".
     - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
diff --git a/base_logic/lib/viewshifts.v b/base_logic/lib/viewshifts.v
index 4648b12d6d123ca3163f3fae78a4b0bde00a3843..02b91ef702c57c96c3e2ce5108825626a2a64c40 100644
--- a/base_logic/lib/viewshifts.v
+++ b/base_logic/lib/viewshifts.v
@@ -69,13 +69,13 @@ Proof.
 Qed.
 
 Lemma vs_inv N E P Q R :
-  nclose N âŠ† E â†’ inv N R âˆ— (â–· R âˆ— P ={E âˆ– nclose N}=> â–· R âˆ— Q) âŠ¢ P ={E}=> Q.
+  â†‘N âŠ† E â†’ inv N R âˆ— (â–· R âˆ— P ={Eâˆ–â†‘N}=> â–· R âˆ— Q) âŠ¢ P ={E}=> Q.
 Proof.
   iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
   iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
   by iApply "Hclose".
 Qed.
 
-Lemma vs_alloc N P : â–· P ={N}=> inv N P.
+Lemma vs_alloc N P : â–· P ={â†‘N}=> inv N P.
 Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
 End vs.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 45b4c8b584b9b61b0902afa127babf279fcc875e..f5ccae49a0813c3e4b6c0cc9dfd0ad0a53c46ea1 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -130,7 +130,7 @@ Section heap.
 
   (** Weakest precondition *)
   Lemma wp_alloc E e v :
-    to_val e = Some v â†’ nclose heapN âŠ† E â†’
+    to_val e = Some v â†’ â†‘heapN âŠ† E â†’
     {{{ heap_ctx }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l â†¦ v }}}.
   Proof.
     iIntros (<-%of_to_val ? Î¦) "#Hinv HÎ¦". rewrite /heap_ctx.
@@ -144,7 +144,7 @@ Section heap.
   Qed.
 
   Lemma wp_load E l q v :
-    nclose heapN âŠ† E â†’
+    â†‘heapN âŠ† E â†’
     {{{ heap_ctx âˆ— â–· l â†¦{q} v }}} Load (Lit (LitLoc l)) @ E
     {{{ RET v; l â†¦{q} v }}}.
   Proof.
@@ -157,7 +157,7 @@ Section heap.
   Qed.
 
   Lemma wp_store E l v' e v :
-    to_val e = Some v â†’ nclose heapN âŠ† E â†’
+    to_val e = Some v â†’ â†‘heapN âŠ† E â†’
     {{{ heap_ctx âˆ— â–· l â†¦ v' }}} Store (Lit (LitLoc l)) e @ E
     {{{ RET LitV LitUnit; l â†¦ v }}}.
   Proof.
@@ -173,7 +173,7 @@ Section heap.
   Qed.
 
   Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
-    to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’ v' â‰  v1 â†’ nclose heapN âŠ† E â†’
+    to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’ v' â‰  v1 â†’ â†‘heapN âŠ† E â†’
     {{{ heap_ctx âˆ— â–· l â†¦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
     {{{ RET LitV (LitBool false); l â†¦{q} v' }}}.
   Proof.
@@ -186,7 +186,7 @@ Section heap.
   Qed.
 
   Lemma wp_cas_suc E l e1 v1 e2 v2 :
-    to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’ nclose heapN âŠ† E â†’
+    to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’ â†‘heapN âŠ† E â†’
     {{{ heap_ctx âˆ— â–· l â†¦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
     {{{ RET LitV (LitBool true); l â†¦ v2 }}}.
   Proof.
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index a859f60734b32d319834deb779d400dd33a47709..3e96e4a1b678512ac256b41f1181217877bff56a 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -162,7 +162,7 @@ Proof.
 Qed.
 
 Lemma recv_split E l P1 P2 :
-  nclose N âŠ† E â†’ recv l (P1 âˆ— P2) ={E}=âˆ— recv l P1 âˆ— recv l P2.
+  â†‘N âŠ† E â†’ recv l (P1 âˆ— P2) ={E}=âˆ— recv l P1 âˆ— recv l P2.
 Proof.
   rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
   iIntros (?). iDestruct 1 as (Î³ P Q i) "(#(%&Hh&Hsts)&HÎ³&#HQ&HQR)".
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index d5f581970f0c530587a1fd943592057712b5e436..8df3af05138ba2b505d1484b70431046c4af3869 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -14,7 +14,7 @@ Lemma barrier_spec (N : namespace) :
                      {{ 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) âˆ§
+    (âˆ€ l P Q, recv l (P âˆ— Q) ={â†‘N}=> recv l P âˆ— recv l Q) âˆ§
     (âˆ€ l P Q, (P -âˆ— Q) âŠ¢ recv l P -âˆ— recv l Q).
 Proof.
   intros HN.
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index e0fba481b36dda57309490ba0a88933cc8ab127b..81959db441eb5fb1edd91f39d2adeba1239c6009 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -18,7 +18,7 @@ Proof. by rewrite /IntoAnd heap_mapsto_op_eq Qp_div_2. Qed.
 
 Lemma tac_wp_alloc Î” Î”' E j e v Î¦ :
   to_val e = Some v â†’
-  (Î” âŠ¢ heap_ctx) â†’ nclose heapN âŠ† E â†’
+  (Î” âŠ¢ heap_ctx) â†’ â†‘heapN âŠ† E â†’
   IntoLaterEnvs Î” Î”' â†’
   (âˆ€ l, âˆƒ Î”'',
     envs_app false (Esnoc Enil j (l â†¦ v)) Î”' = Some Î”'' âˆ§
@@ -33,7 +33,7 @@ Proof.
 Qed.
 
 Lemma tac_wp_load Î” Î”' E i l q v Î¦ :
-  (Î” âŠ¢ heap_ctx) â†’ nclose heapN âŠ† E â†’
+  (Î” âŠ¢ heap_ctx) â†’ â†‘heapN âŠ† E â†’
   IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦{q} v)%I â†’
   (Î”' âŠ¢ Î¦ v) â†’
@@ -47,7 +47,7 @@ Qed.
 
 Lemma tac_wp_store Î” Î”' Î”'' E i l v e v' Î¦ :
   to_val e = Some v' â†’
-  (Î” âŠ¢ heap_ctx) â†’ nclose heapN âŠ† E â†’
+  (Î” âŠ¢ heap_ctx) â†’ â†‘heapN âŠ† E â†’
   IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦ v)%I â†’
   envs_simple_replace i false (Esnoc Enil i (l â†¦ v')) Î”' = Some Î”'' â†’
@@ -62,7 +62,7 @@ Qed.
 
 Lemma tac_wp_cas_fail Î” Î”' E i l q v e1 v1 e2 v2 Î¦ :
   to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
-  (Î” âŠ¢ heap_ctx) â†’ nclose heapN âŠ† E â†’
+  (Î” âŠ¢ heap_ctx) â†’ â†‘heapN âŠ† E â†’
   IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦{q} v)%I â†’ v â‰  v1 â†’
   (Î”' âŠ¢ Î¦ (LitV (LitBool false))) â†’
@@ -76,7 +76,7 @@ Qed.
 
 Lemma tac_wp_cas_suc Î” Î”' Î”'' E i l v e1 v1 e2 v2 Î¦ :
   to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
-  (Î” âŠ¢ heap_ctx) â†’ nclose heapN âŠ† E â†’
+  (Î” âŠ¢ heap_ctx) â†’ â†‘heapN âŠ† E â†’
   IntoLaterEnvs Î” Î”' â†’
   envs_lookup i Î”' = Some (false, l â†¦ v)%I â†’ v = v1 â†’
   envs_simple_replace i false (Esnoc Enil i (l â†¦ v2)) Î”' = Some Î”'' â†’
diff --git a/prelude/base.v b/prelude/base.v
index 4284a89627f3f8c4e0ca1841a21deee2944286e4..51dcdad2f233e0fa907ac48a321b8dd648e4044d 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -726,6 +726,8 @@ End disjoint_list.
 
 Class Filter A B := filter: âˆ€ (P : A â†’ Prop) `{âˆ€ x, Decision (P x)}, B â†’ B.
 
+Class UpClose A B := up_close : A â†’ B.
+Notation "â†‘ x" := (up_close x) (at level 20, format "â†‘ x").
 
 (** * Monadic operations *)
 (** We define operational type classes for the monadic operations bind, join 
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 3f6f8c7fef2bd7525268dc8502952804016cbbfc..bff108e15ae07909fdb2f4a1e8899e85ee336e81 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âŒ }}.
+    â†‘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âŒ }}.
+    â†‘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.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index ab97cc55d2f2881e54f3c06830b98a33f72e6f7f..c5de431e0ab1cd9693f422d67af40f4c03c35ab5 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -90,7 +90,7 @@ Section iris.
   Implicit Types P Q : iProp Î£.
 
   Lemma demo_8 N E P Q R :
-    nclose N âŠ† E â†’
+    â†‘N âŠ† E â†’
     (True -âˆ— P -âˆ— inv N Q -âˆ— True -âˆ— R) âŠ¢ P -âˆ— â–· Q ={E}=âˆ— R.
   Proof.
     iIntros (?) "H HP HQ".