diff --git a/iris b/iris
index 8f33e2828ae7b286adee0071ffa5c40fb4977fcd..f24fd7c35eb4e29c5fccb47200a22b7087fbcb64 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 8f33e2828ae7b286adee0071ffa5c40fb4977fcd
+Subproject commit f24fd7c35eb4e29c5fccb47200a22b7087fbcb64
diff --git a/theories/adequacy.v b/theories/adequacy.v
index 1cd713a040d9b4e1475939d93a4e4d112d556033..e5c53aef9a295b29a269e00b377c3b737a9fe60d 100644
--- a/theories/adequacy.v
+++ b/theories/adequacy.v
@@ -17,7 +17,7 @@ Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. intros [? [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv. split; apply _. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
-  (∀ `{heapG Σ}, {{ heap_ctx }} e {{ v, ■ φ v }}) →
+  (∀ `{heapG Σ}, {{ heap_ctx }} e {{ v, ⌜φ v⌝ }}) →
   adequate e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy Σ). iIntros (?) "Hσ".
diff --git a/theories/frac_borrow.v b/theories/frac_borrow.v
index f68755d8bd070e3514cd8968297116dfc1d7c891..5d6959934113828a5f9c03e98c184ee0090445fc 100644
--- a/theories/frac_borrow.v
+++ b/theories/frac_borrow.v
@@ -7,23 +7,23 @@ Class frac_borrowG Σ := frac_borrowG_inG :> inG Σ fracR.
 
 Definition frac_borrow `{invG Σ, lifetimeG Σ, frac_borrowG Σ} κ (Φ : Qp → iProp Σ) :=
   (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
-                       (q = 1%Qp ∨ ∃ q', (q + q')%Qp = 1%Qp ∗ q'.[κ']))%I.
+                       (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
 Notation "&frac{ κ } P" := (frac_borrow κ P)
   (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
 
 Section frac_borrow.
-
   Context `{invG Σ, lifetimeG Σ, frac_borrowG Σ}.
+  Implicit Types E : coPset.
 
   Global Instance frac_borrow_proper :
     Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_borrow κ).
   Proof. solve_proper. Qed.
   Global Instance frac_borrow_persistent : PersistentP (&frac{κ}φ) := _.
 
-  Lemma borrow_fracture φ `(nclose lftN ⊆ E) κ:
-    lft_ctx ⊢ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
+  Lemma borrow_fracture φ E κ :
+    ↑lftN ⊆ E → lft_ctx ⊢ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
   Proof.
-    iIntros "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
+    iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
     iMod (borrow_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
     - iMod ("Hclose" with "*[-]") as "Hφ"; last first.
       { iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ").
@@ -37,11 +37,12 @@ Section frac_borrow.
       iMod (borrow_fake with "LFT H†"). done. by iApply borrow_share.
   Qed.
 
-  Lemma frac_borrow_atomic_acc `(nclose lftN ⊆ E) κ φ:
-    lft_ctx ⊢ &frac{κ}φ ={E,E∖lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖lftN,E}=∗ True))
-                                      ∨ [†κ] ∗ |={E∖lftN,E}=> True.
+  Lemma frac_borrow_atomic_acc E κ φ :
+    ↑lftN ⊆ E →
+    lft_ctx ⊢ &frac{κ}φ ={E,E∖↑lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖↑lftN,E}=∗ True))
+                                      ∨ [†κ] ∗ |={E∖↑lftN,E}=> True.
   Proof.
-    iIntros "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
+    iIntros (?) "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
     iMod (shr_borrow_acc with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]". done.
     - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
       iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
@@ -49,11 +50,12 @@ Section frac_borrow.
       iApply fupd_intro_mask. set_solver. done.
   Qed.
 
-  Lemma frac_borrow_acc `(nclose lftN ⊆ E) q κ φ:
+  Lemma frac_borrow_acc E q κ φ:
+    ↑lftN ⊆ E →
     lft_ctx ⊢ □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) -∗
     &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
   Proof.
-    iIntros "#LFT #Hφ Hfrac Hκ". unfold frac_borrow.
+    iIntros (?) "#LFT #Hφ Hfrac Hκ". unfold frac_borrow.
     iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
     iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
     iMod (shr_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
diff --git a/theories/heap.v b/theories/heap.v
index 97087b8f529dd3775a849e69f5e64e1007fadafd..5e4a0ba95b7c8756174f5c68ee9d946ec0524a26 100644
--- a/theories/heap.v
+++ b/theories/heap.v
@@ -62,7 +62,7 @@ Section definitions.
   Definition heap_inv : iProp Σ :=
     (∃ (σ:state) hF, ownP σ ∗ own heap_name (● to_heap σ)
                             ∗ own heap_freeable_name (● hF)
-                            ∗ ■ heap_freeable_rel σ hF)%I.
+                            ∗ ⌜heap_freeable_rel σ hF⌝)%I.
   Definition heap_ctx : iProp Σ := inv heapN heap_inv.
 
   Global Instance heap_ctx_persistent : PersistentP heap_ctx.
@@ -95,6 +95,7 @@ Section heap.
   Context {Σ : gFunctors}.
   Implicit Types P Q : iProp Σ.
   Implicit Types σ : state.
+  Implicit Types E : coPset.
 
   (** Allocation *)
   Lemma to_heap_valid σ : ✓ to_heap σ.
@@ -129,10 +130,10 @@ 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_equiv // left_id. }
+    { by rewrite heap_mapsto_op_eq pure_True // left_id. }
     apply (anti_symm (⊢)); last by apply pure_elim_l.
     rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
     eapply pure_elim; [done|]=> /auth_own_valid /=.
@@ -166,20 +167,21 @@ Section heap.
 
   Lemma heap_mapsto_vec_op l q1 q2 vl1 vl2 :
     length vl1 = length vl2 →
-    l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ vl1 = vl2 ∧ l ↦∗{q1+q2} vl1.
+    l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ ⌜vl1 = vl2⌝ ∧ l ↦∗{q1+q2} vl1.
   Proof.
-    iIntros (Hlen%Forall2_same_length); iSplit.
+    intros Hlen%Forall2_same_length. apply (anti_symm (⊢)).
     - revert l. induction Hlen as [|v1 v2 vl1 vl2 _ _ IH]=> l.
       { rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
       rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
-      iDestruct (IH (shift_loc l 1) with "[Hvl1 Hvl2]") as "[% $]"; subst; first by iFrame.
+      iDestruct (IH (shift_loc l 1) with "[Hvl1 Hvl2]") as "[% $]";
+        subst; first by iFrame.
       rewrite (inj_iff (:: vl2)). iApply heap_mapsto_op. by iFrame.
     - iIntros "[% Hl]"; subst. by iApply heap_mapsto_vec_op_eq.
   Qed.
 
   Lemma heap_mapsto_vec_prop_op l q1 q2 n (Φ : list val → iProp Σ) :
-    (∀ vl, Φ vl ⊢ length vl = n) →
-    l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, length vl = n) ⊣⊢ l ↦∗{q1+q2}: Φ.
+    (∀ vl, Φ vl ⊢ ⌜length vl = n⌝) →
+    l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = n⌝) ⊣⊢ l ↦∗{q1+q2}: Φ.
   Proof.
     intros Hlen. iSplit.
     - iIntros "[Hmt1 Hmt2]".
@@ -209,7 +211,7 @@ Section heap.
     by rewrite (big_opL_commute_L (Auth None)) big_opL_commute1 //.
   Qed.
 
-  Lemma inter_lookup_Some i j (n:nat):
+  Lemma inter_lookup_Some i j (n : nat):
     i ≤ j < i+n → inter i n !! j = Excl' ().
   Proof.
     revert i. induction n as [|n IH]=>/= i; first lia.
@@ -322,10 +324,10 @@ Section heap.
     rewrite lookup_init_mem_ne /=; last lia. by rewrite -(shift_loc_0 l) FRESH.
   Qed.
 
-  Lemma wp_alloc E n :
-    nclose heapN ⊆ E → 0 < n →
+  Lemma wp_alloc E n:
+    ↑heapN ⊆ E → 0 < n →
     {{{ heap_ctx }}} Alloc (Lit $ LitInt n) @ E
-    {{{ l vl, RET LitV $ LitLoc l; n = length vl ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
+    {{{ l vl, RET LitV $ LitLoc l; ⌜n = length vl⌝ ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
   Proof.
     iIntros (???) "#Hinv HΦ". rewrite /heap_ctx /heap_inv.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
@@ -368,8 +370,7 @@ Section heap.
   Qed.
 
   Lemma wp_free E (n:Z) l vl :
-    nclose heapN ⊆ E →
-    n = length vl →
+    ↑heapN ⊆ E → n = length vl →
     {{{ heap_ctx ∗ ▷ l ↦∗ vl ∗ ▷ †l…(length vl) }}}
       Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
     {{{ RET LitV LitUnit; True }}}.
@@ -377,7 +378,7 @@ Section heap.
     iIntros (???Φ) "(#Hinv & >Hmt & >Hf) HΦ". rewrite /heap_ctx /heap_inv.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & REL)" "Hclose". iDestruct "REL" as %REL.
     rewrite heap_freeable_eq /heap_freeable_def.
-    iDestruct (own_valid_2 with "[$HhF $Hf]") as % [Hl Hv]%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_valid_discrete_2.
     move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
     apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
     { move: (Hv (l.1)). rewrite Hl. by intros [??]. }
@@ -388,7 +389,7 @@ Section heap.
     { intros i. subst n. eauto using heap_freeable_is_Some. }
     iNext. iIntros "Hσ". iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
     { rewrite heap_mapsto_vec_combine //. iFrame. }
-    iMod (own_update_2 with "[$HhF $Hf]") as "HhF".
+    iMod (own_update_2 with "HhF Hf") as "HhF".
     { apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
     iMod ("Hclose" with "[-HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, _. subst. rewrite Nat2Z.id. iFrame.
@@ -396,12 +397,13 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_lookup l ls q v σ:
-    own heap_name (● to_heap σ) ∗
-    own heap_name (â—¯ {[ l := (q, to_lock_stateR ls, DecAgree v) ]})
-    ⊢ ■ ∃ n' : nat,
-        σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v).
+    own heap_name (● to_heap σ) ⊢
+    own heap_name (◯ {[ l := (q, to_lock_stateR ls, DecAgree v) ]}) -∗
+    ⌜∃ n' : nat,
+        σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
   Proof.
-    rewrite own_valid_2. iDestruct 1 as %[Hl?]%auth_valid_discrete_2.
+    iIntros "H● H◯".
+    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
     iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
     rewrite leibniz_equiv_iff /to_heap lookup_fmap fmap_Some.
     move=> [[[ls'' v'] [??]]]; simplify_eq.
@@ -413,11 +415,12 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_lookup_1 l ls v σ:
-    own heap_name (● to_heap σ) ∗
-    own heap_name (â—¯ {[ l := (1%Qp, to_lock_stateR ls, DecAgree v) ]})
-    ⊢ ■ (σ !! l = Some (ls, v)).
+    own heap_name (● to_heap σ) ⊢
+    own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, DecAgree v) ]}) -∗
+    ⌜σ !! l = Some (ls, v)⌝.
   Proof.
-    rewrite own_valid_2. iDestruct 1 as %[Hl?]%auth_valid_discrete_2.
+    iIntros "H● H◯".
+    iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
     iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
     rewrite leibniz_equiv_iff /to_heap lookup_fmap fmap_Some.
     move=> [[[ls'' v'] [??]] Hincl]; simplify_eq.
@@ -427,14 +430,14 @@ Section heap.
   Qed.
 
   Lemma wp_read_sc E l q v :
-    nclose heapN ⊆ E →
+    ↑heapN ⊆ E →
     {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
     {{{ RET v; l ↦{q} v }}}.
   Proof.
     iIntros (??) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
+    iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
     iApply (wp_read_sc_pst with "[$Hσ]"); first done. iNext. iIntros "Hσ".
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
     iNext. iExists σ, hF. iFrame. eauto.
@@ -454,7 +457,7 @@ Section heap.
   Qed.
 
   Lemma wp_read_na E l q v :
-    nclose heapN ⊆ E →
+    ↑heapN ⊆ E →
     {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
     {{{ RET v; l ↦{q} v }}}.
   Proof.
@@ -462,15 +465,15 @@ Section heap.
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iApply (wp_read_na1_pst E).
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
+    iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
     iMod (heap_read_vs _ 0 1 with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iMod (fupd_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
+    iMod (fupd_intro_mask' (E∖↑heapN) ∅) as "Hclose'"; first set_solver.
     iModIntro. iExists σ, n, v. iFrame. iSplit; [done|]. iIntros "!> Hσ".
     iMod "Hclose'" as "_". iMod ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
     { iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
     iModIntro. clear dependent n σ hF.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
+    iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
     iApply (wp_read_na2_pst with "[$Hσ]"); first done. iNext. iIntros "Hσ".
     iMod (heap_read_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
@@ -490,14 +493,14 @@ Section heap.
   Qed.
 
   Lemma wp_write_sc E l e v v' :
-    nclose heapN ⊆ E → to_val e = Some v →
+    ↑heapN ⊆ E → to_val e = Some v →
     {{{ heap_ctx ∗ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
     {{{ RET LitV LitUnit; l ↦ v }}}.
   Proof.
     iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
+    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
     iApply (wp_write_sc_pst with "[$Hσ]"); [done|]. iNext. iIntros "Hσ".
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
@@ -505,7 +508,7 @@ Section heap.
   Qed.
 
   Lemma wp_write_na E l e v v' :
-    nclose heapN ⊆ E → to_val e = Some v →
+    ↑heapN ⊆ E → to_val e = Some v →
     {{{ heap_ctx ∗ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
     {{{ RET LitV LitUnit; l ↦ v }}}.
   Proof.
@@ -513,15 +516,15 @@ Section heap.
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iApply (wp_write_na1_pst E).
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
+    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
-    iMod (fupd_intro_mask' (E∖heapN) ∅) as "Hclose'"; first set_solver.
+    iMod (fupd_intro_mask' (E∖↑heapN) ∅) as "Hclose'"; first set_solver.
     iModIntro. iExists σ, v'. iSplit; [done|]. iIntros "{$Hσ} !> Hσ".
     iMod "Hclose'" as "_". iMod ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
     { iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
     iModIntro. clear dependent σ hF.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
+    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
     iApply (wp_write_na2_pst with "[$Hσ]"); [done|]. iNext. iIntros "Hσ".
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
@@ -529,7 +532,7 @@ Section heap.
   Qed.
 
   Lemma wp_cas_int_fail E l q z1 e2 v2 zl :
-    nclose heapN ⊆ E → to_val e2 = Some v2 → z1 ≠ zl →
+    ↑heapN ⊆ E → to_val e2 = Some v2 → z1 ≠ zl →
     {{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitInt zl) }}}
       CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
     {{{ RET LitV $ LitInt 0; l ↦{q} (LitV $ LitInt zl) }}}.
@@ -537,7 +540,7 @@ Section heap.
     iIntros (? <-%of_to_val ??) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
+    iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
     iApply (wp_cas_fail_pst with "[$Hσ]"); eauto.
     { by rewrite /= bool_decide_false. }
     iNext. iIntros "Hσ". iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
@@ -545,7 +548,7 @@ Section heap.
   Qed.
 
   Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 v2 l' vl' :
-    nclose heapN ⊆ E → to_val e2 = Some v2 → l1 ≠ l' →
+    ↑heapN ⊆ E → to_val e2 = Some v2 → l1 ≠ l' →
     {{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
       CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
     {{{ RET LitV $ LitInt 0;
@@ -554,9 +557,9 @@ Section heap.
     iIntros (? <-%of_to_val ??) "(#Hinv & >Hl & >Hl' & >Hl1) HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl]") as %[n Hσl].
-    iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl']") as %[n' Hσl'].
-    iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl1]") as %[n1 Hσl1].
+    iDestruct (heap_mapsto_lookup with "Hvalσ Hl") as %[n Hσl].
+    iDestruct (heap_mapsto_lookup with "Hvalσ Hl'") as %[n' Hσl'].
+    iDestruct (heap_mapsto_lookup with "Hvalσ Hl1") as %[n1 Hσl1].
     iApply (wp_cas_fail_pst with "[$Hσ]"); eauto.
     { by rewrite /= bool_decide_false // Hσl1 Hσl'. }
     iNext. iIntros "Hσ ".
@@ -565,7 +568,7 @@ Section heap.
   Qed.
 
   Lemma wp_cas_int_suc E l z1 e2 v2 :
-    nclose heapN ⊆ E → to_val e2 = Some v2 →
+    ↑heapN ⊆ E → to_val e2 = Some v2 →
     {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitInt z1) }}}
       CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
     {{{ RET LitV $ LitInt 1; l ↦ v2 }}}.
@@ -573,7 +576,7 @@ Section heap.
     iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
+    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
     iApply (wp_cas_suc_pst with "[$Hσ]"); eauto.
     { by rewrite /= bool_decide_true. }
     iNext. iIntros "Hσ".
@@ -583,7 +586,7 @@ Section heap.
   Qed.
 
   Lemma wp_cas_loc_suc E l l1 e2 v2 :
-    nclose heapN ⊆ E → to_val e2 = Some v2 →
+    ↑heapN ⊆ E → to_val e2 = Some v2 →
     {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitLoc l1) }}}
       CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
     {{{ RET LitV $ LitInt 1; l ↦ v2 }}}.
@@ -591,7 +594,7 @@ Section heap.
     iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
+    iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
     iApply (wp_cas_suc_pst with "[$Hσ]"); eauto.
     { by rewrite /= bool_decide_true. }
     iNext. iIntros "Hσ".
diff --git a/theories/lang.v b/theories/lang.v
index 8b2f09a9dc79bf9fbb19762bbe1ec713adba7ce5..8acb16ccbf9a777126b621ea696096d1ed6c58ec 100644
--- a/theories/lang.v
+++ b/theories/lang.v
@@ -1,5 +1,4 @@
 From iris.program_logic Require Export language ectx_language ectxi_language.
-From iris.algebra Require Export cofe.
 From iris.prelude Require Export strings.
 From iris.prelude Require Import gmap.
 
diff --git a/theories/lifetime.v b/theories/lifetime.v
index 193be22d9c33f4cd72d93a75ae95384bdc37bc1c..bbc61eef5047531af2275dd194e8d7b84c94fa01 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -42,7 +42,7 @@ Section defs.
     own lft_toks_name (◯ (Cinl <$> omap (Qp_nat_mul q) κ)).
 
   Definition lft_dead (κ : lifetime) : iProp Σ :=
-    (∃ Λ, ■ (∃ n, κ !! Λ = Some (S n)) ∗
+    (∃ Λ, ⌜∃ n, κ !! Λ = Some (S n)⌝ ∗
             own lft_toks_name (◯ {[ Λ := Cinr () ]}))%I.
 
   Definition idx_borrow_own (q : Qp) (i : borrow_idx) :=
@@ -132,42 +132,42 @@ Section lft.
   Qed.
 
   Axiom lft_create :
-    ∀ `(nclose lftN ⊆ E),
-      lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖nclose lftN}▷=∗ [†κ]).
+    ∀ `(↑lftN ⊆ E),
+      lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
 
   Axiom idx_borrow_acc :
-    ∀ `(nclose lftN ⊆ E) q κ i P,
+    ∀ `(↑lftN ⊆ E) q κ i P,
       lft_ctx ⊢ idx_borrow κ i P -∗ idx_borrow_own 1 i
               -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ idx_borrow_own 1 i ∗ q.[κ]).
   Axiom idx_borrow_atomic_acc :
-    ∀ `(nclose lftN ⊆ E) q κ i P,
+    ∀ `(↑lftN ⊆ E) q κ i P,
       lft_ctx ⊢ idx_borrow κ i P -∗ idx_borrow_own q i
-         ={E,E∖lftN}=∗
-            ▷ P ∗ (▷ P ={E∖lftN,E}=∗ idx_borrow_own q i) ∨
-            [†κ] ∗ (|={E∖lftN,E}=> idx_borrow_own q i).
+         ={E,E∖↑lftN}=∗
+            ▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_borrow_own q i) ∨
+            [†κ] ∗ (|={E∖↑lftN,E}=> idx_borrow_own q i).
 
   (** Basic borrows  *)
   Axiom borrow_create :
-    ∀ `(nclose lftN ⊆ E) κ P, lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
-  Axiom borrow_fake : ∀ `(nclose lftN ⊆ E) κ P, lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
+    ∀ `(↑lftN ⊆ E) κ P, lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
+  Axiom borrow_fake : ∀ `(↑lftN ⊆ E) κ P, lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
   Axiom borrow_split :
-    ∀ `(nclose lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
+    ∀ `(↑lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
   Axiom borrow_combine :
-    ∀ `(nclose lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}P -∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
+    ∀ `(↑lftN ⊆ E) κ P Q, lft_ctx ⊢ &{κ}P -∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
   Axiom borrow_acc_strong :
-    ∀ `(nclose lftN ⊆ E) q κ P,
+    ∀ `(↑lftN ⊆ E) q κ P,
       lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗
-      ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
+      ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ ↑lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
   Axiom borrow_acc_atomic_strong :
-    ∀ `(nclose lftN ⊆ E) κ P,
-      lft_ctx ⊢ &{κ}P ={E,E∖lftN}=∗
-        (▷ P ∗ ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E∖lftN,E}=∗ &{κ}Q) ∨
-        [†κ] ∗ |={E∖lftN,E}=> True.
+    ∀ `(↑lftN ⊆ E) κ P,
+      lft_ctx ⊢ &{κ}P ={E,E∖↑lftN}=∗
+        (▷ P ∗ ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ ↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ}Q) ∨
+        [†κ] ∗ |={E∖↑lftN,E}=> True.
   Axiom borrow_reborrow' :
-    ∀ `(nclose lftN ⊆ E) κ κ' P, κ ≼ κ' →
+    ∀ `(↑lftN ⊆ E) κ κ' P, κ ≼ κ' →
       lft_ctx ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
   Axiom borrow_unnest :
-    ∀ `(nclose lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E}▷=∗ &{κ ⋅ κ'}P.
+    ∀ `(↑lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E}▷=∗ &{κ ⋅ κ'}P.
 
   (*** Derived lemmas  *)
 
@@ -176,7 +176,7 @@ Section lft.
     rewrite /lft_own /lft_dead.
     iIntros "Hl Hr". iDestruct "Hr" as (Λ) "[HΛ Hr]".
     iDestruct "HΛ" as %[n HΛ].
-    iDestruct (own_valid_2 with "[$Hl $Hr]") as %Hval. iPureIntro.
+    iDestruct (own_valid_2 with "Hl Hr") as %Hval. iPureIntro.
     generalize (Hval Λ).
     by rewrite lookup_op lookup_singleton lookup_fmap lookup_omap HΛ.
   Qed.
@@ -224,34 +224,37 @@ Section lft.
     FromSep q.[κ1⋅κ2] q.[κ1] q.[κ2].
   Proof. by rewrite /FromSep lft_own_op. Qed.
 
-  Lemma borrow_acc E q κ P : nclose lftN ⊆ E →
-      lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
+  Lemma borrow_acc E q κ P :
+    ↑lftN ⊆ E →
+    lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
   Proof.
     iIntros (?) "#LFT HP Htok".
     iMod (borrow_acc_strong with "LFT HP Htok") as "[HP Hclose]". done.
     iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>_$".
   Qed.
 
-  Lemma borrow_exists {A} `(nclose lftN ⊆ E) κ (Φ : A → iProp Σ) {_:Inhabited A}:
+  Lemma borrow_exists {A} E κ (Φ : A → iProp Σ) {_:Inhabited A}:
+    ↑lftN ⊆ E →
     lft_ctx ⊢ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
   Proof.
-    iIntros "#LFT Hb".
+    iIntros (?) "#LFT Hb".
     iMod (borrow_acc_atomic_strong with "LFT Hb") as "[[HΦ Hclose]|[H† Hclose]]". done.
     - iDestruct "HΦ" as (x) "HΦ". iExists x. iApply "Hclose". iIntros "{$HΦ}!>_?". eauto.
     - iMod "Hclose" as "_". iExists inhabitant. by iApply (borrow_fake with "LFT").
   Qed.
 
-  Lemma borrow_or `(nclose lftN ⊆ E) κ P Q:
-    lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
+  Lemma borrow_or E κ P Q:
+    ↑lftN ⊆ E → lft_ctx ⊢ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
   Proof.
-    iIntros "#LFT H". rewrite uPred.or_alt.
+    iIntros (?) "#LFT H". rewrite uPred.or_alt.
     iMod (borrow_exists with "LFT H") as ([]) "H"; auto.
   Qed.
 
-  Lemma borrow_persistent `(nclose lftN ⊆ E) `{PersistentP _ P} κ q:
+  Lemma borrow_persistent E `{PersistentP _ P} κ q:
+    ↑lftN ⊆ E →
     lft_ctx ⊢ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
   Proof.
-    iIntros "#LFT Hb Htok".
+    iIntros (?) "#LFT Hb Htok".
     iMod (borrow_acc with "LFT Hb Htok") as "[#HP Hob]". done.
     by iMod ("Hob" with "HP") as "[_$]".
   Qed.
@@ -263,8 +266,8 @@ Typeclasses Opaque borrow.
 (*** Inclusion and shortening. *)
 
 Definition lft_incl `{invG Σ, lifetimeG Σ} κ κ' : iProp Σ :=
-  (□((∀ q, q.[κ] ={lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={lftN}=∗ q.[κ])) ∗
-     ([†κ'] ={lftN}=∗ [†κ])))%I.
+  (□((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
+     ([†κ'] ={↑lftN}=∗ [†κ])))%I.
 
 Infix "⊑" := lft_incl (at level 60) : C_scope.
 
@@ -273,17 +276,18 @@ Section incl.
 
   Global Instance lft_incl_persistent κ κ': PersistentP (κ ⊑ κ') := _.
 
-  Lemma lft_incl_acc `(nclose lftN ⊆ E) κ κ' q:
+  Lemma lft_incl_acc E κ κ' q:
+    ↑lftN ⊆ E →
     κ ⊑ κ' ⊢ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
   Proof.
-    iIntros "#[H _] Hq". iApply fupd_mask_mono. eassumption.
+    iIntros (?) "#[H _] Hq". iApply fupd_mask_mono. eassumption.
     iMod ("H" with "*Hq") as (q') "[Hq' Hclose]". iExists q'.
     iIntros "{$Hq'}!>Hq". iApply fupd_mask_mono. eassumption. by iApply "Hclose".
   Qed.
 
-  Lemma lft_incl_dead `(nclose lftN ⊆ E) κ κ': κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
+  Lemma lft_incl_dead E κ κ': ↑lftN ⊆ E → κ ⊑ κ' ⊢ [†κ'] ={E}=∗ [†κ].
   Proof.
-    iIntros "#[_ H] Hq". iApply fupd_mask_mono. eassumption. by iApply "H".
+    iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono. eassumption. by iApply "H".
   Qed.
 
   Lemma lft_le_incl κ κ': κ' ≼ κ → True ⊢ κ ⊑ κ'.
@@ -338,11 +342,11 @@ Section incl.
     - iIntros "?". by iDestruct (lft_not_dead_static with "[-]") as "[]".
   Qed.
 
-  Lemma reborrow `(nclose lftN ⊆ E) P κ κ':
-    lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
+  Lemma reborrow E P κ κ':
+    ↑lftN ⊆ E → lft_ctx ⊢ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
   Proof.
-    iIntros "#LFT #H⊑ HP". iMod (borrow_reborrow' with "LFT HP") as "[Hκ' H∋]".
-      done. by exists κ'.
+    iIntros (?) "#LFT #H⊑ HP".
+    iMod (borrow_reborrow' with "LFT HP") as "[Hκ' H∋]". done. by exists κ'.
     iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
     { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
     iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
diff --git a/theories/lifting.v b/theories/lifting.v
index 26ba40bde604251a87f843733bc2bee604c51629..e3f6b3faa03db2b8b2890b81d1fa0b281f97c752 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -26,8 +26,8 @@ Lemma wp_alloc_pst E σ n:
   0 < n →
   {{{ ▷ ownP σ }}} Alloc (Lit $ LitInt n) @ E
   {{{ l σ', RET LitV $ LitLoc l;
-      ■ (∀ m, σ !! (shift_loc l m) = None) ∗
-      ■ (∃ vl, n = length vl ∧ init_mem l vl σ = σ') ∗
+      ⌜∀ m, σ !! (shift_loc l m) = None⌝ ∗
+      ⌜∃ vl, n = length vl ∧ init_mem l vl σ = σ'⌝ ∗
       ownP σ' }}}.
 Proof.
   iIntros (? Φ) "HP HΦ". iApply (wp_lift_atomic_head_step _ σ); eauto.
@@ -66,7 +66,7 @@ Proof.
 Qed.
 
 Lemma wp_read_na1_pst E l Φ :
-  (|={E,∅}=> ∃ σ n v, σ !! l = Some(RSt $ n, v) ∧
+  (|={E,∅}=> ∃ σ n v, ⌜σ !! l = Some(RSt $ n, v)⌝ ∧
      ▷ ownP σ ∗
      ▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=∗
           WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }}))
@@ -97,7 +97,7 @@ Proof.
 Qed.
 
 Lemma wp_write_na1_pst E l v Φ :
-  (|={E,∅}=> ∃ σ v', σ !! l = Some(RSt 0, v') ∧
+  (|={E,∅}=> ∃ σ v', ⌜σ !! l = Some(RSt 0, v')⌝ ∧
      ▷ ownP σ ∗
      ▷ (ownP (<[l:=(WSt, v')]>σ) ={∅,E}=∗
        WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}))
diff --git a/theories/memcpy.v b/theories/memcpy.v
index 4fb6d9a2082cd800978fbecb70b91125c817b5c3..e945532fe282f8afd8951121fe4b6157cf8ddbb1 100644
--- a/theories/memcpy.v
+++ b/theories/memcpy.v
@@ -18,7 +18,7 @@ Notation "e1 <-[ i ]{ n } ! e2" :=
    format "e1  <-[ i ]{ n }  ! e2") : lrust_expr_scope.
 
 Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
-  nclose heapN ⊆ E →
+  ↑heapN ⊆ E →
   length vl1 = n → length vl2 = n →
   {{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
     #l1 <-{n} !#l2 @ E
diff --git a/theories/perm.v b/theories/perm.v
index fbe763f4eddc1fbc07f8b492dcce6365ae5c91e6..6638a70128ee47876cc01a20a9090de32354ec1b 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -24,14 +24,14 @@ Section perm.
     from_option (λ v, ty.(ty_own) tid [v]) False%I (eval_expr ν).
 
   Definition extract (κ : lifetime) (ρ : perm) : perm :=
-    λ tid, ([†κ] ={lftN}=∗ ρ tid)%I.
+    λ tid, ([†κ] ={↑lftN}=∗ ρ tid)%I.
 
   Definition tok (κ : lifetime) (q : Qp) : perm :=
     λ _, q.[κ]%I.
 
 
   Definition killable (κ : lifetime) : perm :=
-    λ _, (□ (1.[κ] ={⊤,⊤∖nclose lftN}▷=∗ [†κ]))%I.
+    λ _, (□ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]))%I.
 
   Definition incl (κ κ' : lifetime) : perm :=
     λ _, (κ ⊑ κ')%I.
@@ -105,7 +105,7 @@ Section has_type.
   Qed.
 
   Lemma has_type_wp E (ν : expr) ty tid (Φ : val -> iProp _) :
-    (ν ◁ ty)%P tid ∗ (∀ (v : val), eval_expr ν = Some v ∗ (v ◁ ty)%P tid ={E}=∗ Φ v)
+    (ν ◁ ty)%P tid ∗ (∀ (v : val), ⌜eval_expr ν = Some v⌝ ∗ (v ◁ ty)%P tid ={E}=∗ Φ v)
     ⊢ WP ν @ E {{ Φ }}.
   Proof.
     iIntros "[H◁ HΦ]". setoid_rewrite has_type_value. unfold has_type.
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index 4d646f391561e4efcc01630bd7c6b9de769e1b76..93eebced650654f2a41012465ea82cbe38dccf1b 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -125,7 +125,7 @@ Section props.
       iDestruct "H" as (vl) "[H↦ H]". iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)".
       subst. rewrite heap_mapsto_vec_app -heap_freeable_op_eq.
       iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
-      iAssert (â–· (length vl1 = ty_size ty1))%I with "[#]" as ">EQ".
+      iAssert (▷ ⌜length vl1 = ty_size ty1⌝)%I with "[#]" as ">EQ".
       { iNext. by iApply ty_size_eq. }
       iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
       + iExists _. iSplitR. done. iFrame. iExists _. by iFrame.
@@ -136,7 +136,7 @@ Section props.
       iExists l. iSplitR. done. rewrite -heap_freeable_op_eq. iFrame.
       iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
       iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
-      iAssert (â–· (length vl1 = ty_size ty1))%I with "[#]" as ">EQ".
+      iAssert (▷ ⌜length vl1 = ty_size ty1⌝)%I with "[#]" as ">EQ".
       { iNext. by iApply ty_size_eq. }
       iDestruct "EQ" as %->. iFrame. iExists vl1, vl2. iFrame. auto.
   Qed.
@@ -275,7 +275,7 @@ Section props.
     destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
     iDestruct "Hown" as (l') "[EQ [Hown Hf]]". iDestruct "EQ" as %[=]. subst l'.
-    iApply (fupd_mask_mono lftN). done.
+    iApply (fupd_mask_mono (↑lftN)). done.
     iMod (borrow_create with "LFT Hown") as "[Hbor Hext]". done.
     iSplitL "Hbor". by simpl; eauto.
     iMod (borrow_create with "LFT Hf") as "[_ Hf]". done.
@@ -291,7 +291,7 @@ Section props.
     destruct (eval_expr ν) as [[[|l|]|]|];
       try by (iDestruct "H" as "[]" || iDestruct "H" as (l) "[% _]").
     iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. subst l'.
-    iApply (fupd_mask_mono lftN). done.
+    iApply (fupd_mask_mono (↑lftN)). done.
     iMod (reborrow with "LFT Hord H") as "[H Hextr]". done.
     iModIntro. iSplitL "H". iExists _. by eauto.
     iIntros "H†". iMod ("Hextr" with "H†"). simpl. auto.
@@ -299,8 +299,8 @@ Section props.
 
   Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ').
   Proof.
-    iIntros (tid) "#LFT _ Htok". iApply fupd_mask_mono. done.
-    iMod (borrow_create with "LFT [$Htok]") as "[Hbor Hclose]". reflexivity.
+    iIntros (tid) "#LFT _ Htok". iApply (fupd_mask_mono (↑lftN)). done.
+    iMod (borrow_create with "LFT [$Htok]") as "[Hbor Hclose]". done.
     iMod (borrow_fracture (λ q', (q * q').[κ'])%I with "LFT [Hbor]") as "Hbor". done.
     { by rewrite Qp_mult_1_r. }
     iSplitL "Hbor". iApply (frac_borrow_incl with "LFT Hbor").
diff --git a/theories/proofmode.v b/theories/proofmode.v
index ade46392b711c4e74f78101efd0c833e3c0d7c29..7c1cde572271bba6a50706ece3235c540fba019d 100644
--- a/theories/proofmode.v
+++ b/theories/proofmode.v
@@ -21,7 +21,7 @@ Global Instance into_and_mapsto_vec l q vl :
 Proof. by rewrite /IntoAnd heap_mapsto_vec_op_split. Qed.
 
 Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
-  (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → 0 < n →
+  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → 0 < n →
   IntoLaterEnvs Δ Δ' →
   (∀ l vl, n = length vl → ∃ Δ'',
     envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
@@ -39,7 +39,7 @@ Proof.
 Qed.
 
 Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
-  (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → n = length vl →
+  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → n = length vl →
   IntoLaterEnvs Δ Δ' →
   envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
   envs_delete i1 false Δ' = Δ'' →
@@ -57,7 +57,7 @@ Proof.
 Qed.
 
 Lemma tac_wp_read Δ Δ' E i l q v o Φ :
-  (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
+  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
   IntoLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   (Δ' ⊢ |={E}=> Φ v) →
@@ -76,7 +76,7 @@ Qed.
 
 Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
   to_val e = Some v' →
-  (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
+  (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
   IntoLaterEnvs Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
diff --git a/theories/shr_borrow.v b/theories/shr_borrow.v
index 65714ea6a06397e9faf6d4776af86ed8627f722f..a4eed050443b69c26127202cbdd43105340e49d9 100644
--- a/theories/shr_borrow.v
+++ b/theories/shr_borrow.v
@@ -16,17 +16,18 @@ Section shared_borrows.
   Proof. solve_proper. Qed.
   Global Instance shr_borrow_persistent : PersistentP (&shr{κ} P) := _.
 
-  Lemma borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=∗ &shr{κ}P.
+  Lemma borrow_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
   Proof.
-    iIntros "HP". unfold borrow. iDestruct "HP" as (i) "(#?&Hown)".
+    iIntros (?) "HP". unfold borrow. iDestruct "HP" as (i) "(#?&Hown)".
     iExists i. iFrame "#". iApply inv_alloc. auto.
   Qed.
 
-  Lemma shr_borrow_acc `(nclose lftN ⊆ E) κ :
-    lft_ctx ⊢ &shr{κ}P ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ True) ∨
-                          [†κ] ∗ |={E∖lftN,E}=> True.
+  Lemma shr_borrow_acc E κ :
+    ↑lftN ⊆ E →
+    lft_ctx ⊢ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
+               [†κ] ∗ |={E∖↑lftN,E}=> True.
   Proof.
-    iIntros "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
+    iIntros (?) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
     iInv lftN as (q') ">Hq'" "Hclose".
     rewrite -(Qp_div_2 q') /idx_borrow_own -op_singleton auth_frag_op own_op.
     iDestruct "Hq'" as "[Hq'0 Hq'1]". iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
@@ -35,10 +36,11 @@ Section shared_borrows.
     - iRight. iFrame. iIntros "!>". by iMod "Hclose".
   Qed.
 
-  Lemma shr_borrow_acc_tok `(nclose lftN ⊆ E) q κ :
-    lft_ctx ⊢ &shr{κ}P -∗ q.[κ] ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ q.[κ]).
+  Lemma shr_borrow_acc_tok E q κ :
+    ↑lftN ⊆ E →
+    lft_ctx ⊢ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
   Proof.
-    iIntros "#LFT #Hshr Hκ".
+    iIntros (?) "#LFT #Hshr Hκ".
     iMod (shr_borrow_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]". done.
     - iIntros "!>HP". by iMod ("Hclose" with "HP").
     - iDestruct (lft_own_dead with "Hκ H†") as "[]".
diff --git a/theories/tl_borrow.v b/theories/tl_borrow.v
index b85f4058125674ef1c1f310483c8cc9bfab62953..7dcd10f861cb306edbaf19a7b2cdd3be6d0c14a9 100644
--- a/theories/tl_borrow.v
+++ b/theories/tl_borrow.v
@@ -20,17 +20,17 @@ Section tl_borrow.
     intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
   Qed.
 
-  Lemma borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P.
+  Lemma borrow_tl κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &tl{κ|tid|N}P.
   Proof.
-    iIntros "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
+    iIntros (?) "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
     iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
   Qed.
 
   Lemma tl_borrow_acc q κ E F :
-    nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F →
+    ↑lftN ⊆ E → ↑tlN ⊆ E → ↑N ⊆ F →
     lft_ctx ⊢ &tl{κ|tid|N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
-            ▷P ∗ tl_own tid (F ∖ N) ∗
-            (▷P -∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F).
+            ▷P ∗ tl_own tid (F ∖ ↑N) ∗
+            (▷P -∗ tl_own tid (F ∖ ↑N) ={E}=∗ q.[κ] ∗ tl_own tid F).
   Proof.
     iIntros (???) "#LFT#HP Hκ Htlown".
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
diff --git a/theories/type.v b/theories/type.v
index ebc124bc32a755adcd645aa66ae94439131b6e1d..abbe4b63cca0514469476e4d44287e2356b8d9db 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -11,7 +11,7 @@ Class iris_typeG Σ := Iris_typeG {
   type_frac_borrowG Σ :> frac_borrowG Σ
 }.
 
-Definition mgmtE := nclose tlN ∪ lftN.
+Definition mgmtE := ↑tlN ∪ ↑lftN.
 Definition lrustN := nroot .@ "lrust".
 
 (* [perm] is defined here instead of perm.v in order to define [cont] *)
@@ -30,7 +30,7 @@ Record type :=
     ty_dup_persistent tid vl : ty_dup → PersistentP (ty_own tid vl);
     ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
 
-    ty_size_eq tid vl : ty_own tid vl ⊢ length vl = ty_size;
+    ty_size_eq tid vl : ty_own tid vl ⊢ ⌜length vl = ty_size⌝;
     (* The mask for starting the sharing does /not/ include the
        namespace N, for allowing more flexibility for the user of
        this type (typically for the [own] type). AFAIK, there is no
@@ -40,8 +40,8 @@ Record type :=
        invariants, which does not need the mask.  Moreover, it is
        more consistent with thread-local tokens, which we do not
        give any. *)
-    ty_share E N κ l tid q : mgmtE ⊥ nclose N → mgmtE ⊆ E →
-      lft_ctx ⊢ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid N l ∗ q.[κ];
+    ty_share E N κ l tid q : mgmtE ⊥ ↑N → mgmtE ⊆ E →
+      lft_ctx ⊢ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗ ty_shr κ tid (↑N) l ∗ q.[κ];
     ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
       lft_ctx ⊢ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
     ty_shr_acc κ tid E F l q :
@@ -59,7 +59,7 @@ Record simple_type `{iris_typeG Σ} :=
   { st_size : nat;
     st_own : thread_id → list val → iProp Σ;
 
-    st_size_eq tid vl : st_own tid vl ⊢ length vl = st_size;
+    st_size_eq tid vl : st_own tid vl ⊢ ⌜length vl = st_size⌝;
     st_own_persistent tid vl : PersistentP (st_own tid vl) }.
 Global Existing Instance st_own_persistent.
 
@@ -99,7 +99,7 @@ Next Obligation.
     iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
     + iNext. iExists _. by iFrame.
     + iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
-      iAssert (â–· (length vl = length vl'))%I as ">%".
+      iAssert (▷ ⌜length vl = length vl'⌝)%I as ">%".
       { iNext.
         iDestruct (st_size_eq with "Hown") as %->.
         iDestruct (st_size_eq with "Hown'") as %->. done. }
@@ -137,15 +137,15 @@ Section types.
   Next Obligation. intros. iIntros "_ []". Qed.
 
   Program Definition unit : type :=
-    {| st_size := 0; st_own tid vl := (vl = [])%I |}.
+    {| st_size := 0; st_own tid vl := ⌜vl = []⌝%I |}.
   Next Obligation. iIntros (tid vl) "%". simpl. by subst. Qed.
 
   Program Definition bool : type :=
-    {| st_size := 1; st_own tid vl := (∃ z:bool, vl = [ #z ])%I |}.
+    {| st_size := 1; st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
   Program Definition int : type :=
-    {| st_size := 1; st_own tid vl := (∃ z:Z, vl = [ #z ])%I |}.
+    {| st_size := 1; st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
   Program Definition own (q : Qp) (ty : type) :=
@@ -157,7 +157,7 @@ Section types.
 
             Since this assertion is timeless, this should not cause
             problems. *)
-         (∃ l:loc, vl = [ #l ] ∗ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ †{q}l…ty.(ty_size))%I;
+         (∃ l:loc, ⌜vl = [ #l ]⌝ ∗ ▷ l ↦∗: ty.(ty_own) tid ∗ ▷ †{q}l…ty.(ty_size))%I;
        ty_shr κ tid E l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
             ∀ q', □ (q'.[κ] ={mgmtE ∪ E, mgmtE}▷=∗ ty.(ty_shr) κ tid E l' ∗ q'.[κ]))%I
@@ -177,11 +177,11 @@ Section types.
     iMod (borrow_split with "LFT Hb2") as "[Hb2 _]". set_solver.
     iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
     rewrite /borrow. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
-    iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid N l')%I
+    iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
     iExists l'. iIntros "!>{$Hbf}".  iIntros (q'') "!#Htok".
     iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
-    replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
+    replace ((mgmtE ∪ ↑N) ∖ ↑N) with mgmtE by set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (&{κ}▷ l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
       { rewrite /borrow. iExists i. eauto. }
@@ -209,7 +209,7 @@ Section types.
   Program Definition uniq_borrow (κ:lifetime) (ty:type) :=
     {| ty_size := 1; ty_dup := false;
        ty_own tid vl :=
-         (∃ l:loc, vl = [ #l ] ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
+         (∃ l:loc, ⌜vl = [ #l ]⌝ ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
        ty_shr κ' tid E l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
             ∀ q', □ (q'.[κ ⋅ κ']
@@ -229,11 +229,11 @@ Section types.
     rewrite heap_mapsto_vec_singleton.
     iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
     rewrite {1}/borrow. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
-    iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty (κ⋅κ') tid N l')%I
+    iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty (κ⋅κ') tid (↑N) l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
     iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
     iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
-    replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
+    replace ((mgmtE ∪ ↑N) ∖ ↑N) with mgmtE by set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
       { rewrite /borrow. eauto. }
@@ -262,14 +262,14 @@ Section types.
   Program Definition shared_borrow (κ : lifetime) (ty : type) : type :=
     {| st_size := 1;
        st_own tid vl :=
-         (∃ (l:loc), vl = [ #l ] ∗ ty.(ty_shr) κ tid lrustN l)%I |}.
+         (∃ (l:loc), ⌜vl = [ #l ]⌝ ∗ ty.(ty_shr) κ tid (↑lrustN) l)%I |}.
   Next Obligation.
     iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
 
   Lemma split_prod_mt tid ty1 ty2 q l :
     (l ↦∗{q}: λ vl,
-       ∃ vl1 vl2, vl = vl1 ++ vl2 ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
+       ∃ vl1 vl2, ⌜vl = vl1 ++ vl2⌝ ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I
        ⊣⊢ l ↦∗{q}: ty1.(ty_own) tid ∗ shift_loc l ty1.(ty_size) ↦∗{q}: ty2.(ty_own) tid.
   Proof.
     iSplit; iIntros "H".
@@ -287,9 +287,9 @@ Section types.
     {| ty_size := ty1.(ty_size) + ty2.(ty_size);
        ty_dup := ty1.(ty_dup) && ty2.(ty_dup);
        ty_own tid vl := (∃ vl1 vl2,
-         vl = vl1 ++ vl2 ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
+         ⌜vl = vl1 ++ vl2⌝ ∗ ty1.(ty_own) tid vl1 ∗ ty2.(ty_own) tid vl2)%I;
        ty_shr κ tid E l :=
-         (∃ E1 E2, ■ (E1 ⊥ E2 ∧ E1 ⊆ E ∧ E2 ⊆ E) ∗
+         (∃ E1 E2, ⌜E1 ⊥ E2 ∧ E1 ⊆ E ∧ E2 ⊆ E⌝ ∗
             ty1.(ty_shr) κ tid E1 l ∗
             ty2.(ty_shr) κ tid E2 (shift_loc l ty1.(ty_size)))%I |}.
   Next Obligation. intros ty1 ty2 tid vl [Hdup1 Hdup2]%andb_True. apply _. Qed.
@@ -304,7 +304,7 @@ Section types.
     iMod (borrow_split with "LFT H") as "[H1 H2]". set_solver.
     iMod (ty1.(ty_share) _ (N .@ 1) with "LFT H1 Htok") as "[? Htok]". solve_ndisj. done.
     iMod (ty2.(ty_share) _ (N .@ 2) with "LFT H2 Htok") as "[? $]". solve_ndisj. done.
-    iModIntro. iExists (N .@ 1). iExists (N .@ 2). iFrame.
+    iModIntro. iExists (↑N .@ 1). iExists (↑N .@ 2). iFrame.
     iPureIntro. split. solve_ndisj. split; apply nclose_subseteq.
   Qed.
   Next Obligation.
@@ -326,18 +326,18 @@ Section types.
     destruct (Qp_lower_bound q1 q2) as (qq & q'1 & q'2 & -> & ->). iExists qq.
     iDestruct "H1" as (vl1) "[H↦1 H1]". iDestruct "H2" as (vl2) "[H↦2 H2]".
     rewrite -!heap_mapsto_vec_op_eq !split_prod_mt.
-    iAssert (â–· (length vl1 = ty1.(ty_size)))%I with "[#]" as ">%".
+    iAssert (▷ ⌜length vl1 = ty1.(ty_size)⌝)%I with "[#]" as ">%".
     { iNext. by iApply ty_size_eq. }
-    iAssert (â–· (length vl2 = ty2.(ty_size)))%I with "[#]" as ">%".
+    iAssert (▷ ⌜length vl2 = ty2.(ty_size)⌝)%I with "[#]" as ">%".
     { iNext. by iApply ty_size_eq. }
     iDestruct "H↦1" as "[H↦1 H↦1f]". iDestruct "H↦2" as "[H↦2 H↦2f]".
     iIntros "!>". iSplitL "H↦1 H1 H↦2 H2".
     - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
     - iIntros "[H1 H2]".
       iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
-      iAssert (â–· (length vl1' = ty1.(ty_size)))%I with "[#]" as ">%".
+      iAssert (▷ ⌜length vl1' = ty1.(ty_size)⌝)%I with "[#]" as ">%".
       { iNext. by iApply ty_size_eq. }
-      iAssert (â–· (length vl2' = ty2.(ty_size)))%I with "[#]" as ">%".
+      iAssert (▷ ⌜length vl2' = ty2.(ty_size)⌝)%I with "[#]" as ">%".
       { iNext. by iApply ty_size_eq. }
       iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
       rewrite !heap_mapsto_vec_op; try by congruence.
@@ -350,7 +350,7 @@ Section types.
 
   Lemma split_sum_mt l tid q tyl :
     (l ↦∗{q}: λ vl,
-         ∃ (i : nat) vl', vl = #i :: vl' ∗ ty_own (nth i tyl emp) tid vl')%I
+         ∃ (i : nat) vl', ⌜vl = #i :: vl'⌝ ∗ ty_own (nth i tyl emp) tid vl')%I
     ⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: ty_own (nth i tyl emp) tid.
   Proof.
     iSplit; iIntros "H".
@@ -369,7 +369,7 @@ Section types.
   Proof. intros. constructor; done. Qed.
 
   Lemma sum_size_eq n tid i tyl vl {Hn : LstTySize n tyl} :
-    ty_own (nth i tyl emp) tid vl ⊢ length vl = n.
+    ty_own (nth i tyl emp) tid vl ⊢ ⌜length vl = n⌝.
   Proof.
     iIntros "Hown". iDestruct (ty_size_eq with "Hown") as %->.
     revert Hn. rewrite /LstTySize List.Forall_forall /= =>Hn.
@@ -380,7 +380,7 @@ Section types.
   Program Definition sum {n} (tyl : list type) {_:LstTySize n tyl} :=
     {| ty_size := S n; ty_dup := forallb ty_dup tyl;
        ty_own tid vl :=
-         (∃ (i : nat) vl', vl = #i :: vl' ∗ (nth i tyl emp).(ty_own) tid vl')%I;
+         (∃ (i : nat) vl', ⌜vl = #i :: vl'⌝ ∗ (nth i tyl emp).(ty_own) tid vl')%I;
        ty_shr κ tid N l :=
          (∃ (i : nat), (&frac{κ} λ q, l ↦{q} #i) ∗
                (nth i tyl emp).(ty_shr) κ tid N (shift_loc l 1))%I
@@ -436,12 +436,12 @@ Section types.
   Qed.
 
   Program Definition uninit : type :=
-    {| st_size := 1; st_own tid vl := (length vl = 1%nat)%I |}.
+    {| st_size := 1; st_own tid vl := ⌜length vl = 1%nat⌝%I |}.
   Next Obligation. done. Qed.
 
   Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
     {| ty_size := 1; ty_dup := false;
-       ty_own tid vl := (∃ f, vl = [f] ∗
+       ty_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗
           ∀ vl, ρ vl tid -∗ tl_own tid ⊤
                  -∗ WP f (map of_val vl) {{λ _, False}})%I;
        ty_shr κ tid N l := True%I |}.
@@ -459,7 +459,7 @@ Section types.
      needs a Send closure). *)
   Program Definition fn {A n} (ρ : A -> vec val n → @perm Σ) : type :=
     {| st_size := 1;
-       st_own tid vl := (∃ f, vl = [f] ∗ ∀ x vl,
+       st_own tid vl := (∃ f, ⌜vl = [f]⌝ ∗ ∀ x vl,
          {{ ρ x vl tid ∗ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
   Next Obligation.
     iIntros (x n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
diff --git a/theories/type_incl.v b/theories/type_incl.v
index e2fdf2af343a3a10518f9cf01a6549e7fff5dcc5..a7f34971a9d507f9054a2fa4269782233b34d7cd 100644
--- a/theories/type_incl.v
+++ b/theories/type_incl.v
@@ -16,7 +16,7 @@ Section ty_incl.
           object when it is shared. We place this property under the
           hypothesis that [ty2.(ty_shr)] holds, so that the [!] type
           is still included in any other. *)
-                  ty2.(ty_shr) κ tid E l ∗ ty1.(ty_size) = ty2.(ty_size)).
+                  ty2.(ty_shr) κ tid E l ∗ ⌜ty1.(ty_size) = ty2.(ty_size)⌝).
 
   Global Instance ty_incl_refl ρ : Reflexive (ty_incl ρ).
   Proof. iIntros (ty tid) "__!>". iSplit; iIntros "!#"; eauto. Qed.
diff --git a/theories/typing.v b/theories/typing.v
index bf0398bf219a0eabc4ffe3958671c293c70740da..d7f653f80e211bf4527722798dc9d92c50eae018 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -142,7 +142,7 @@ Section typing.
   Proof.
     iIntros (tid) "!#(_&_&(Hextr&Htok&Hend)&$)".
     iApply wp_fupd. iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr".
-    iApply (wp_frame_step_l with "[-]"); try done.
+    iApply (wp_frame_step_l _ (⊤ ∖ ↑lftN) with "[-]"); try done.
     iDestruct ("Hend" with "Htok") as "$". by wp_seq.
     iIntros (v) "[#Hκ _]". by iApply fupd_mask_mono; last iApply "Hextr".
   Qed.
@@ -173,10 +173,10 @@ Section typing.
   Qed.
 
   Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
-    ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
+    ∀ ν tid Φ E, mgmtE ∪ ↑lrustN ⊆ E →
       lft_ctx ⊢ ρ1 ν tid -∗ tl_own tid ⊤ -∗
       (∀ (l:loc) vl q,
-        (length vl = ty.(ty_size) ∗ eval_expr ν = Some #l ∗ l ↦∗{q} vl ∗
+        (⌜length vl = ty.(ty_size)⌝ ∗ ⌜eval_expr ν = Some #l⌝ ∗ l ↦∗{q} vl ∗
          |={E}▷=> (ty.(ty_own) tid vl ∗ (l ↦∗{q} vl ={E}=∗ ρ2 ν tid ∗ tl_own tid ⊤)))
        -∗ Φ #l)
       -∗ WP ν @ E {{ Φ }}.
@@ -188,7 +188,7 @@ Section typing.
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
-    iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
+    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
     iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
     rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
@@ -202,7 +202,7 @@ Section typing.
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦ & >H†)".
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">Hlen".
+    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">Hlen".
       by rewrite ty.(ty_size_eq). iDestruct "Hlen" as %Hlen.
     iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
     rewrite /has_type Hνv. iExists _. iSplit. done. iSplitR "H†".
@@ -224,7 +224,7 @@ Section typing.
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     iMod (borrow_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
-    iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
+    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
     iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
     iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]". by iExists _; iFrame.
@@ -240,11 +240,11 @@ Section typing.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l') "[Heq #Hshr]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
-    rewrite (union_difference_L (nclose lrustN) ⊤); last done.
+    rewrite (union_difference_L (↑lrustN) ⊤); last done.
     setoid_rewrite ->tl_own_union; try set_solver. iDestruct "Htl" as "[Htl ?]".
     iMod (ty_shr_acc with "LFT Hshr [$Htok $Htl]") as (q'') "[H↦ Hclose']"; try set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
-    iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
+    iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
     iModIntro. iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
     iMod ("Hclose'" with "[H↦]") as "[Htok $]". iExists _; by iFrame.
@@ -296,9 +296,9 @@ Section typing.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
     iSpecialize ("Hown" $! _ with "Htok2").
     iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
-    - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q'''} v ∗ v = #vl)%I); try done.
+    - iApply (wp_frame_step_l _ (↑heapN) _ (λ v, l ↦{q'''} v ∗ ⌜v = #vl⌝)%I); try done.
       iSplitL "Hown"; last by wp_read; eauto.
-      iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
+      iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ (↑heapN));
         last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
     - iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
       iMod ("Hclose'" with "[$H↦]") as "Htok'".
@@ -346,9 +346,9 @@ Section typing.
     iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
     iSpecialize ("Hown" $! _ with "Htok").
     iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose' Hclose''"; last first.
-    - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q''} v ∗ v = #l')%I); try done.
+    - iApply (wp_frame_step_l _ (↑heapN) _ (λ v, l ↦{q''} v ∗ ⌜v = #l'⌝)%I); try done.
       iSplitL "Hown"; last by wp_read; eauto.
-      iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
+      iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ (↑heapN));
         last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
     - iIntros (v) "([#Hshr Htok] & H↦ & %)". subst.
       iMod ("Hclose''" with "Htok") as "Htok".
@@ -358,10 +358,10 @@ Section typing.
   Qed.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
-    ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
+    ∀ ν tid Φ E, mgmtE ∪ (↑lrustN) ⊆ E →
       lft_ctx ⊢ ρ1 ν tid -∗
       (∀ (l:loc) vl,
-         (length vl = ty.(ty_size) ∗ eval_expr ν = Some #l ∗ l ↦∗ vl ∗
+         (⌜length vl = ty.(ty_size)⌝ ∗ ⌜eval_expr ν = Some #l⌝ ∗ l ↦∗ vl ∗
          ∀ vl', l ↦∗ vl' ∗ ▷ (ty.(ty_own) tid vl') ={E}=∗ ρ2 ν tid)
          -∗ Φ #l)
       -∗ WP ν @ E {{ Φ }}.