diff --git a/opam b/opam
new file mode 100644
index 0000000000000000000000000000000000000000..3c8ddd9c17f82f4253711864c2c990e88b2b472e
--- /dev/null
+++ b/opam
@@ -0,0 +1,17 @@
+opam-version: "1.2"
+name: "coq-lambda-rust"
+version: "dev"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The RustBelt Team"
+homepage: "http://plv.mpi-sws.org/rustbelt/"
+bug-reports: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq/issues"
+license: "BSD"
+dev-repo: "https://gitlab.mpi-sws.org/FP/lambdaRust-coq"
+build: [
+  [make "-j%{jobs}%"]
+]
+install: [make "install"]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
+depends: [
+  "https://gitlab.mpi-sws.org/FP/iris-coq/" { (= "dev")) }
+]
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/derived.v b/theories/derived.v
index a7c7ad94ce5ee4ff8392f8947580535d00056f9d..1a2180deea64c381d029206151e663d689430993 100644
--- a/theories/derived.v
+++ b/theories/derived.v
@@ -25,35 +25,35 @@ Lemma wp_lam E xl e e' el Φ :
   Forall (λ ei, is_Some (to_val ei)) el →
   Closed (xl +b+ []) e →
   subst_l xl el e = Some e' →
-  ▷ WP e' @ E {{ Φ }} ⊢ WP App (Lam xl e) el @ E {{ Φ }}.
+  ▷ WP e' @ E {{ Φ }} -∗ WP App (Lam xl e) el @ E {{ Φ }}.
 Proof. iIntros (???) "?". by iApply (wp_rec _ _ BAnon). Qed.
 
 Lemma wp_let E x e1 e2 v Φ :
   to_val e1 = Some v →
   Closed (x :b: []) e2 →
-  ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
+  ▷ WP subst' x e1 e2 @ E {{ Φ }} -∗ WP Let x e1 e2 @ E {{ Φ }}.
 Proof. eauto using wp_lam. Qed.
 
 Lemma wp_seq E e1 e2 v Φ :
   to_val e1 = Some v →
   Closed [] e2 →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
+  ▷ WP e2 @ E {{ Φ }} -∗ WP Seq e1 e2 @ E {{ Φ }}.
 Proof. iIntros (??) "?". by iApply (wp_let _ BAnon). Qed.
 
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
+Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) -∗ WP Skip @ E {{ Φ }}.
 Proof. iIntros. iApply wp_seq. done. iNext. by iApply wp_value. Qed.
 
 Lemma wp_le E (n1 n2 : Z) P Φ :
-  (n1 ≤ n2 → P ⊢ ▷ |={E}=> Φ (LitV true)) →
-  (n2 < n1 → P ⊢ ▷ |={E}=> Φ (LitV false)) →
-  P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+  (n1 ≤ n2 → P -∗ ▷ |={E}=> Φ (LitV true)) →
+  (n2 < n1 → P -∗ ▷ |={E}=> Φ (LitV false)) →
+  P -∗ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
 Proof.
   intros. rewrite -wp_bin_op //; [].
   destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
 Qed.
 
 Lemma wp_if E (b : bool) e1 e2 Φ :
-  (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I
-  ⊢ WP If (Lit b) e1 e2 @ E {{ Φ }}.
+  (if b then ▷ WP e1 @ E {{ Φ }} else ▷ WP e2 @ E {{ Φ }})%I -∗
+  WP If (Lit b) e1 e2 @ E {{ Φ }}.
 Proof. iIntros "?". by destruct b; iApply wp_case. Qed.
 End derived.
diff --git a/theories/frac_borrow.v b/theories/frac_borrow.v
index f68755d8bd070e3514cd8968297116dfc1d7c891..64f595dd8a222f28043d677142a05060dc638249 100644
--- a/theories/frac_borrow.v
+++ b/theories/frac_borrow.v
@@ -1,5 +1,6 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import lib.fractional.
 From iris.algebra Require Import frac.
 From lrust Require Export lifetime shr_borrow.
 
@@ -7,41 +8,42 @@ 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{κ}φ) := _.
+  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φ").
         iApply lft_incl_refl. }
       iSplitL. by iExists 1%Qp; iFrame; auto.
-      iIntros "!>H† Hφ!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
+      iIntros "!>H† HΦ!>". iNext. iDestruct "HΦ" as (q') "(HΦ & _ & [%|Hκ])". by subst.
       iDestruct "Hκ" as (q'') "[_ Hκ]".
       iDestruct (lft_own_dead with "Hκ H†") as "[]".
-    - iMod ("Hclose" with "*") as "Hφ"; last first.
+    - iMod ("Hclose" with "*") as "HΦ"; last first.
       iExists γ, κ. iSplitR. by iApply lft_incl_refl.
       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,66 +51,73 @@ Section frac_borrow.
       iApply fupd_intro_mask. set_solver. done.
   Qed.
 
-  Lemma frac_borrow_acc `(nclose lftN ⊆ E) q κ φ:
-    lft_ctx ⊢ □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) -∗
-    &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
+  Lemma frac_borrow_acc_strong 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.
-    iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)".
-    destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
+    iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & Hq)".
+    destruct (Qp_lower_bound (qκ'/2) (qΦ/2)) as (qq & qκ'0 & qΦ0 & Hqκ' & HqΦ).
     iExists qq.
-    iAssert (▷ φ qq ∗ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
-    { iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. }
-    rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'.
+    iAssert (▷ Φ qq ∗ ▷ Φ (qΦ0 + qΦ / 2))%Qp%I with "[HΦqΦ]" as "[$ HqΦ]".
+    { iNext. rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ. iApply "HΦ". by rewrite assoc. }
+    rewrite -{1}(Qp_div_2 qΦ) {1}HqΦ -assoc {1}Hqκ'.
     iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
-    iMod ("Hclose'" with "[Hqφ Hq Hown Hκq]") as "Hκ1".
+    iMod ("Hclose'" with "[HqΦ Hq Hown Hκq]") as "Hκ1".
     { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]".
       - subst. iExists qq. iIntros "{$Hκq}!%".
-        by rewrite (comm _ qφ0) -assoc (comm _ qφ0) -Hqφ Qp_div_2.
+        by rewrite (comm _ qΦ0) -assoc (comm _ qΦ0) -HqΦ Qp_div_2.
       - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
-        rewrite lft_own_frac_op. iIntros "{$Hκq $Hq'κ}!%".
-        by rewrite assoc (comm _ _ qq) assoc -Hqφ Qp_div_2. }
-    clear Hqφ qφ qφ0. iIntros "!>Hqφ".
+        iIntros "{$Hκq $Hq'κ}!%". by rewrite assoc (comm _ _ qq) assoc -HqΦ Qp_div_2. }
+    clear HqΦ qΦ qΦ0. iIntros "!>HqΦ".
     iMod (shr_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
-    iDestruct "H" as (qφ) "(Hφqφ & >Hown & >[%|Hq])".
+    iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & >[%|Hq])".
     { subst. iCombine "Hown" "Hownq" as "Hown".
       by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
-    iDestruct "Hq" as (q') "[Hqφq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
-    iDestruct (own_valid with "Hown") as %Hval. iDestruct "Hqφq'" as %Hqφq'.
+    iDestruct "Hq" as (q') "[HqΦq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown".
+    iDestruct (own_valid with "Hown") as %Hval. iDestruct "HqΦq'" as %HqΦq'.
     assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-].
-    { change (qφ + qq ≤ 1)%Qc in Hval. apply Qp_eq in Hqφq'. simpl in Hval, Hqφq'.
-      rewrite <-Hqφq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
+    { change (qΦ + qq ≤ 1)%Qc in Hval. apply Qp_eq in HqΦq'. simpl in Hval, HqΦq'.
+      rewrite <-HqΦq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
       destruct Hval as [Hval|Hval].
       by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. }
     - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
       iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
-      iMod ("Hclose'" with "[Hqφ Hφqφ Hown Hq'qκ]") as "Hqκ2".
-      { iNext. iExists (qφ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "Hφ"; iFrame.
+      iMod ("Hclose'" with "[HqΦ HΦqΦ Hown Hq'qκ]") as "Hqκ2".
+      { iNext. iExists (qΦ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "HΦ"; iFrame.
         iRight. iExists _. iIntros "{$Hq'qκ}!%".
-        revert Hqφq'. rewrite !Qp_eq. move=>/=<-. ring. }
-      iApply "Hclose". iFrame. rewrite Hqκ' !lft_own_frac_op. by iFrame.
-    - iMod ("Hclose'" with "[Hqφ Hφqφ Hown]") as "Hqκ2".
-      { iNext. iExists (qφ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "Hφ"; iFrame. auto. }
-      iApply "Hclose". rewrite -{2}(Qp_div_2 qκ') {2}Hqκ' !lft_own_frac_op. by iFrame.
+        revert HqΦq'. rewrite !Qp_eq. move=>/=<-. ring. }
+      iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
+    - iMod ("Hclose'" with "[HqΦ HΦqΦ Hown]") as "Hqκ2".
+      { iNext. iExists (qΦ ⋅ qq)%Qp. iFrame. iSplitL. by iApply "HΦ"; iFrame. auto. }
+      iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
+  Qed.
+
+  Lemma frac_borrow_acc E q κ `{Fractional _ Φ} :
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
+  Proof.
+    iIntros (?) "LFT". iApply (frac_borrow_acc_strong with "LFT"). done.
+    iIntros "!#*". rewrite fractional. iSplit; auto.
   Qed.
 
-  Lemma frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -∗ &frac{κ}φ.
+  Lemma frac_borrow_shorten κ κ' Φ: κ ⊑ κ' -∗ &frac{κ'}Φ -∗ &frac{κ}Φ.
   Proof.
-    iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame.
-    iApply lft_incl_trans. iFrame.
+    iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[#H⊑ ?]". iExists γ, κ0. iFrame.
+    iApply (lft_incl_trans with "Hκκ' []"). auto.
   Qed.
 
   Lemma frac_borrow_incl κ κ' q:
-    lft_ctx ⊢ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
+    lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
   Proof.
     iIntros "#LFT#Hbor!#". iSplitR.
     - iIntros (q') "Hκ'".
-      iMod (frac_borrow_acc with "LFT [] Hbor Hκ'") as (q'') "[>? Hclose]". done.
-      + iIntros "/=!#*". rewrite Qp_mult_plus_distr_r lft_own_frac_op. iSplit; auto.
-      + iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
+      iMod (frac_borrow_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
+      iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
     - iIntros "H†'".
       iMod (frac_borrow_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
       iDestruct "H" as (q') "[>Hκ' _]".
diff --git a/theories/heap.v b/theories/heap.v
index 97087b8f529dd3775a849e69f5e64e1007fadafd..dbe54f5eaef42f33da9cedf4d8cd42159c0237c1 100644
--- a/theories/heap.v
+++ b/theories/heap.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import cmra_big_op gmap frac dec_agree.
 From iris.algebra Require Import csum excl auth.
-From iris.base_logic Require Import big_op lib.invariants.
+From iris.base_logic Require Import big_op lib.invariants lib.fractional.
 From iris.proofmode Require Export tactics.
 From lrust Require Export lifting.
 Import uPred.
@@ -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 σ.
@@ -117,22 +118,35 @@ Section heap.
   Global Instance heap_mapsto_timeless l q v : TimelessP (l↦{q}v).
   Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
 
+  Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
+  Proof.
+    intros p q. by rewrite heap_mapsto_eq -own_op
+      -auth_frag_op op_singleton pair_op dec_agree_idemp.
+  Qed.
+  Global Instance heap_mapsto_as_fractional l q v:
+    AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
+  Proof. done. Qed.
+
   Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦∗{q} vl).
   Proof. apply _. Qed.
 
-  Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
-  Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
-
-  Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ∗ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
+  Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
   Proof.
-    by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton pair_op dec_agree_idemp.
+    intros p q. rewrite /heap_mapsto_vec -big_sepL_sepL.
+    by setoid_rewrite (fractional (Φ := λ q, _ ↦{q} _)%I).
   Qed.
+  Global Instance heap_mapsto_vec_as_fractional l q vl:
+    AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
+  Proof. done. Qed.
+
+  Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
+  Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. 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 -(fractional (Φ := λ q, l ↦{q} _)%I) 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 /=.
@@ -158,28 +172,23 @@ Section heap.
     by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
   Qed.
 
-  Lemma heap_mapsto_vec_op_eq l q1 q2 vl :
-    l ↦∗{q1} vl ∗ l ↦∗{q2} vl ⊣⊢ l ↦∗{q1+q2} vl.
-  Proof.
-    rewrite /heap_mapsto_vec -big_sepL_sepL. by setoid_rewrite heap_mapsto_op_eq.
-  Qed.
-
   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.
+    - by iIntros "[% [$ Hl2]]"; subst.
   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]".
@@ -187,19 +196,11 @@ Section heap.
       iDestruct (Hlen with "Hown") as %?.
       iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op; last congruence.
       iDestruct "Hmt" as "[_ Hmt]". iExists vl. by iFrame.
-    - iIntros "Hmt". setoid_rewrite <-heap_mapsto_vec_op_eq.
-      iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
+    - iIntros "Hmt". iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
       iDestruct (Hlen with "Hown") as %?.
       iSplitL "Hmt1 Hown"; iExists _; by iFrame.
   Qed.
 
-  Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ l ↦{q/2} v ∗ l ↦{q/2} v.
-  Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
-
-  Lemma heap_mapsto_vec_op_split l q vl :
-    l ↦∗{q} vl ⊣⊢ l ↦∗{q/2} vl ∗ l ↦∗{q/2} vl.
-  Proof. by rewrite heap_mapsto_vec_op_eq Qp_div_2. Qed.
-
   Lemma heap_mapsto_vec_combine l q vl :
     vl ≠ [] →
     l ↦∗{q} vl ⊣⊢ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
@@ -209,7 +210,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 +323,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 +369,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 +377,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 +388,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 +396,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 +414,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 +429,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 +456,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 +464,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 +492,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 +507,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 +515,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 +531,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 +539,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 +547,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 +556,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 +567,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 +575,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 +585,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 +593,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/lft_contexts.v b/theories/lft_contexts.v
new file mode 100644
index 0000000000000000000000000000000000000000..1f78d25a05f871297b04d1f91eecab7feea52964
--- /dev/null
+++ b/theories/lft_contexts.v
@@ -0,0 +1,20 @@
+From iris.proofmode Require Import tactics.
+From lrust Require Export type lifetime.
+
+Section lft_contexts.
+
+  Context `{iris_typeG Σ}.
+
+  Inductive ext_lft_ctx_elt :=
+  | 
+
+  Definition ext_lft_ctx := Qp → iProp Σ.
+
+  Global Instance empty_ext_lft_ctx : Empty ext_lft_ctx := λ _, True%I.
+
+  
+
+
+  Definition int_lft_ctx := iProp Σ.
+
+  
\ No newline at end of file
diff --git a/theories/lifting.v b/theories/lifting.v
index 26ba40bde604251a87f843733bc2bee604c51629..4fead4c2ce18f526efcbda81e9a51528f48e79fa 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -13,11 +13,11 @@ Implicit Types ef : option expr.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} -∗ WP fill K e @ E {{ Φ }}.
 Proof. exact: wp_ectx_bind. Qed.
 
 Lemma wp_bindi {E e} Ki Φ :
-  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
+  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} -∗
      WP fill_item Ki e @ E {{ Φ }}.
 Proof. exact: weakestpre.wp_bind. Qed.
 
@@ -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,11 +66,11 @@ 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 {{ Φ }}))
-  ⊢ WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
+          WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }})) -∗
+  WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
   iIntros "HΦP". iApply (wp_lift_head_step E); auto.
   iMod "HΦP" as (σ n v) "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
@@ -97,11 +97,11 @@ 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 {{ Φ }}))
-  ⊢ WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
+       WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }})) -∗
+  WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
 Proof.
   iIntros "HΦP". iApply (wp_lift_head_step E); auto.
   iMod "HΦP" as (σ v') "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
@@ -147,8 +147,8 @@ Lemma wp_rec E e f xl erec erec' el Φ :
   Forall (λ ei, is_Some (to_val ei)) el →
   Closed (f :b: xl +b+ []) erec →
   subst_l xl el erec = Some erec' →
-  ▷ WP subst' f e erec' @ E {{ Φ }}
-  ⊢ WP App e el @ E {{ Φ }}.
+  ▷ WP subst' f e erec' @ E {{ Φ }} -∗
+  WP App e el @ E {{ Φ }}.
 Proof.
   iIntros (-> ???) "?". iApply wp_lift_pure_det_head_step; subst; eauto.
   by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
@@ -156,7 +156,7 @@ Qed.
 
 Lemma wp_bin_op E op l1 l2 l' Φ :
   bin_op_eval op l1 l2 = Some l' →
-  ▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
+  ▷ (|={E}=> Φ (LitV l')) -∗ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto.
@@ -166,7 +166,7 @@ Qed.
 Lemma wp_case E i e el Φ :
   0 ≤ i →
   nth_error el (Z.to_nat i) = Some e →
-  ▷ WP e @ E {{ Φ }} ⊢ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
+  ▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
 Proof.
   iIntros (??) "?". iApply wp_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
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..ae364946073f7bd5797991f96d897acd2c3843ed 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,12 +105,13 @@ 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)
-    ⊢ WP ν @ E {{ Φ }}.
+    (ν ◁ 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.
+    iIntros "H◁ HΦ". setoid_rewrite has_type_value. unfold has_type.
     destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]". simpl.
-    iMod ("HΦ" $! v with "[$H◁]") as "HΦ". done.
+    iMod ("HΦ" $! v with "[] H◁") as "HΦ". done.
     iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
       forall (Φ v EQν); try done.
     - inversion EQν. subst. wp_value. auto.
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index 4d646f391561e4efcc01630bd7c6b9de769e1b76..ff589d0e07b642e47a02b056df9dc9e5a5dd8459 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -10,13 +10,13 @@ Section defs.
 
   (* Definitions *)
   Definition perm_incl (ρ1 ρ2 : perm) :=
-    ∀ tid, lft_ctx ⊢ ρ1 tid ={⊤}=∗ ρ2 tid.
+    ∀ tid, lft_ctx -∗ ρ1 tid ={⊤}=∗ ρ2 tid.
 
   Global Instance perm_equiv : Equiv perm :=
     λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
 
   Definition borrowing κ (ρ ρ1 ρ2 : perm) :=
-    ∀ tid, lft_ctx ⊢ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ (κ ∋ ρ1)%P tid.
+    ∀ tid, lft_ctx -∗ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ (κ ∋ ρ1)%P tid.
 
 End defs.
 
@@ -93,15 +93,13 @@ Section props.
 
   Lemma perm_tok_plus κ q1 q2 :
     tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
-  Proof.
-    rewrite /tok /sep /=; split; iIntros (tid) "_ ?"; rewrite lft_own_frac_op //.
-  Qed.
+  Proof. rewrite /tok /sep /=; split; by iIntros (tid) "_ [$$]". Qed.
 
   Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
   Proof. iIntros (tid) "_ _!>". iApply lft_incl_refl. Qed.
 
   Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
-  Proof. iIntros (tid) "_ [#?#?]!>". iApply lft_incl_trans. auto. Qed.
+  Proof. iIntros (tid) "_ [#?#?]!>". iApply (lft_incl_trans with "[] []"); auto. Qed.
 
   Lemma perm_incl_share q ν κ ty :
     ν ◁ &uniq{κ} ty ∗ q.[κ] ⇒ ν ◁ &shr{κ} ty ∗ q.[κ].
@@ -125,7 +123,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 +134,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 +273,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 +289,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 +297,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..dbd10fe695c5eca23088bfa4f57ee6822605890d 100644
--- a/theories/proofmode.v
+++ b/theories/proofmode.v
@@ -12,16 +12,8 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (iResUR Σ).
 
-Global Instance into_and_mapsto l q v :
-  IntoAnd false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
-Proof. by rewrite /IntoAnd heap_mapsto_op_split. Qed.
-
-Global Instance into_and_mapsto_vec l q vl :
-  IntoAnd false (l ↦∗{q} vl) (l ↦∗{q/2} vl) (l ↦∗{q/2} 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 +31,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 +49,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 +68,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..5987de8da012e84c88c41313c7e049e2d33d515e 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,16 +36,17 @@ 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 "[]".
   Qed.
 
-  Lemma shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
+  Lemma shr_borrow_shorten κ κ': κ ⊑ κ' -∗ &shr{κ'}P -∗ &shr{κ}P.
   Proof.
     iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
       by iApply (idx_borrow_shorten with "H⊑").
diff --git a/theories/tl_borrow.v b/theories/tl_borrow.v
index 6cfa358b330c64c7c491a038ba20b09f7a5cfd39..11f628e1b302c299206b0e6be002d0efd5c2b217 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 →
-    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).
+    ↑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).
   Proof.
     iIntros (???) "#LFT#HP Hκ Htlown".
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
@@ -40,7 +40,7 @@ Section tl_borrow.
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
-  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ',tid,N}P -∗ &tl{κ,tid,N}P.
+  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' -∗ &tl{κ'|tid|N}P -∗ &tl{κ,tid,N}P.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
     iApply (idx_borrow_shorten with "Hκκ' H").
diff --git a/theories/type.v b/theories/type.v
index ebc124bc32a755adcd645aa66ae94439131b6e1d..21b23768763691738926f3dee9381080c1734e70 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,13 +40,13 @@ 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;
+      lft_ctx -∗ κ' ⊑ κ -∗ ty_shr κ tid E l -∗ ty_shr κ' tid E' l;
     ty_shr_acc κ tid E F l q :
       ty_dup → mgmtE ∪ F ⊆ E →
-      lft_ctx ⊢ ty_shr κ tid F l -∗
+      lft_ctx -∗ ty_shr κ tid F l -∗
         q.[κ] ∗ tl_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
            (▷l ↦∗{q'}: ty_own tid ={E}=∗ q.[κ] ∗ tl_own tid F)
   }.
@@ -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.
 
@@ -91,20 +91,16 @@ Qed.
 Next Obligation.
   intros st κ tid E F l q ??. iIntros "#LFT #Hshr[Hlft $]".
   iDestruct "Hshr" as (vl) "[Hf Hown]".
-  iMod (frac_borrow_acc with "LFT [] Hf Hlft") as (q') "[Hmt Hclose]";
-    first set_solver.
-  - iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_vec_op_eq.
-    iSplit; auto.
-  - iModIntro. rewrite {1}heap_mapsto_vec_op_split. iExists _.
-    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 ">%".
-      { iNext.
-        iDestruct (st_size_eq with "Hown") as %->.
-        iDestruct (st_size_eq with "Hown'") as %->. done. }
-      iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
-      iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
+  iMod (frac_borrow_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
+  iModIntro. iExists _. 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 ">%".
+    { iNext.
+      iDestruct (st_size_eq with "Hown") as %->.
+      iDestruct (st_size_eq with "Hown'") as %->. done. }
+    iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
+    iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
 Qed.
 
 End type.
@@ -137,15 +133,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 +153,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 +173,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,11 +205,11 @@ 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'.[κ ⋅ κ']
-               ={mgmtE ∪ E, mgmtE}▷=∗ ty.(ty_shr) (κ⋅κ') tid E l' ∗ q'.[κ⋅κ']))%I
+               ={mgmtE ∪ E, ↑tlN}▷=∗ ty.(ty_shr) (κ⋅κ') tid E l' ∗ q'.[κ⋅κ']))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -229,26 +225,29 @@ 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".
+    iApply (step_fupd_mask_mono (mgmtE ∪ ↑N) _ _ ((mgmtE ∪ ↑N) ∖ ↑N ∖ ↑lftN)).
+    { assert (nclose lftN ⊥ ↑tlN) by solve_ndisj. set_solver. } set_solver.
     iMod (inv_open with "Hinv") as "[INV Hclose]". 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. }
       iMod (borrow_unnest with "LFT Hb") as "Hb". set_solver.
       iIntros "!>". iNext. iMod "Hb".
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done.
+      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done. set_solver.
       iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
-    - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
+    - iMod (step_fupd_mask_mono _ _ _ _ True%I with "[]") as "Hclose'"; last first.
+      iIntros "!>". iNext. iMod "Hclose'" as "_".
+      iMod ("Hclose" with "[]") as "_"; by eauto. eauto. done. set_solver.
   Qed.
   Next Obligation.
     intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
-    iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ) as "#Hκ0".
-    { iApply lft_incl_lb. iSplit.
+    iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ)%I as "#Hκ0".
+    { iApply (lft_incl_lb with "[] []").
       - iApply lft_le_incl. by exists κ'.
-      - iApply lft_incl_trans. iSplit; last done.
+      - iApply (lft_incl_trans with "[] Hκ").
         iApply lft_le_incl. exists κ0. apply (comm _). }
     iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]"). iIntros (q) "!#Htok".
     iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
@@ -262,14 +261,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 +286,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 +303,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.
@@ -325,19 +324,19 @@ Section types.
     iMod (ty2.(ty_shr_acc) with "LFT H2 [$Htok2 $Htl2]") as (q2) "[H2 Hclose2]". done. set_solver.
     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 ">%".
+    rewrite !split_prod_mt.
+    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 +349,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 +368,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 +379,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
@@ -412,21 +411,17 @@ Section types.
     intros n tyl Hn κ tid E F l q Hdup%Is_true_eq_true ?.
     iIntros "#LFT #H[[Htok1 Htok2] Htl]".
     setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
-    iMod (frac_borrow_acc with "LFT [] Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
-    { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; eauto. }
+    iMod (frac_borrow_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
     iMod ((nth i tyl emp).(ty_shr_acc) with "LFT Hshr [Htok2 $Htl]")
       as (q'2) "[Hownq Hclose']"; try done.
     { edestruct nth_in_or_default as [| ->]; last done.
       rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left. }
     destruct (Qp_lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
-    iExists q'. iModIntro.
-    rewrite -{1}heap_mapsto_op_eq -{1}heap_mapsto_vec_prop_op;
-      last (by intros; apply sum_size_eq, Hn).
+    rewrite -{1}heap_mapsto_vec_prop_op; last (by intros; apply sum_size_eq, Hn).
     iDestruct "Hownq" as "[Hownq1 Hownq2]". iDestruct "Hown" as "[Hown1 Hown2]".
-    iSplitL "Hown1 Hownq1".
+    iExists q'. iModIntro. iSplitL "Hown1 Hownq1".
     - iNext. iExists i. by iFrame.
     - iIntros "H". iDestruct "H" as (i') "[Hown1 Hownq1]".
-      rewrite (lft_own_split _ q).
       iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_op.
       iDestruct "Hown" as "[>#Hi Hown]". iDestruct "Hi" as %[= ->%Z_of_nat_inj].
       iMod ("Hclose" with "Hown") as "$".
@@ -436,12 +431,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 +454,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..8ce12186257af5fd71507beb90230f11716a4aa8 100644
--- a/theories/type_incl.v
+++ b/theories/type_incl.v
@@ -9,17 +9,17 @@ Section ty_incl.
   Context `{iris_typeG Σ}.
 
   Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
-    ∀ tid, lft_ctx ⊢ ρ tid ={⊤}=∗
+    ∀ tid, lft_ctx -∗ ρ tid ={⊤}=∗
       (□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ∗
       (□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
        (* [ty_incl] needs to prove something about the length of the
           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.
+  Proof. iIntros (ty tid) "_ _!>". iSplit; iIntros "!#"; eauto. Qed.
 
   Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
     ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ∗ θ) ty1 ty3.
@@ -74,10 +74,9 @@ Section ty_incl.
     iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
       by iApply (borrow_shorten with "Hincl").
-    - iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ) as "#Hincl'".
-      { iApply lft_incl_lb. iSplit.
-        - iApply lft_incl_trans. iSplit; last done.
-          iApply lft_le_incl. by exists κ.
+    - iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ)%I as "#Hincl'".
+      { iApply (lft_incl_lb with "[] []").
+        - iApply (lft_incl_trans with "[] Hincl"). iApply lft_le_incl. by exists κ.
         - iApply lft_le_incl. exists κ1. by apply (comm _). }
       iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
       iFrame. iIntros (q') "!#Htok".
@@ -191,7 +190,7 @@ Section ty_incl.
     ty_incl ρ (sum tyl1) (sum tyl2).
   Proof.
     iIntros (DUP FA tid) "#LFT #Hρ". rewrite /sum /=. iSplitR "".
-    - assert (Hincl : lft_ctx ⊢ ρ tid ={⊤}=∗
+    - assert (Hincl : lft_ctx -∗ ρ tid ={⊤}=∗
          (□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl
                   → (nth i tyl2 ∅%T).(ty_own) tid vl)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
@@ -202,7 +201,7 @@ Section ty_incl.
       iMod (Hincl with "LFT Hρ") as "#Hincl". iIntros "!>!#*H".
       iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
         by iApply "Hincl".
-    - assert (Hincl : lft_ctx ⊢ ρ tid ={⊤}=∗
+    - assert (Hincl : lft_ctx -∗ ρ tid ={⊤}=∗
          (□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l
                      → (nth i tyl2 ∅%T).(ty_shr) κ tid E l)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
diff --git a/theories/typing.v b/theories/typing.v
index bf0398bf219a0eabc4ffe3958671c293c70740da..4ba6d657725781a82e924c1517b27c2da6f014ae 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -87,7 +87,7 @@ Section typing.
   Lemma typed_valuable (ν : expr) ty:
     typed_step_ty (ν ◁ ty) ν ty.
   Proof.
-    iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "[_$]".
+    iIntros (tid) "!#(_&_&H&$)". iApply (has_type_wp with "[$H]"). by iIntros (v) "_ $".
   Qed.
 
   Lemma typed_plus e1 e2 ρ1 ρ2:
@@ -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.
@@ -165,7 +165,7 @@ Section typing.
     typed_step (ν ◁ own 1 ty) (Free #ty.(ty_size) ν) (λ _, top).
   Proof.
     iIntros (tid) "!#(#HEAP&_&H◁&$)". wp_bind ν.
-    iApply (has_type_wp with "[$H◁]"). iIntros (v) "[_ H◁]!>".
+    iApply (has_type_wp with "[$H◁]"). iIntros (v) "_ H◁ !>".
     rewrite has_type_value.
     iDestruct "H◁" as (l) "(Hv & H↦∗: & >H†)". iDestruct "Hv" as %[=->].
     iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
@@ -173,10 +173,10 @@ Section typing.
   Qed.
 
   Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
-    ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
-      lft_ctx ⊢ ρ1 ν tid -∗ tl_own tid ⊤ -∗
+    ∀ ν 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 {{ Φ }}.
@@ -184,11 +184,11 @@ Section typing.
   Lemma consumes_copy_own ty q:
     ty.(ty_dup) → consumes ty (λ ν, ν ◁ own q ty)%P (λ ν, ν ◁ own q ty)%P.
   Proof.
-    iIntros (? ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "[- $H◁]").
-    iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    iIntros (? ν tid Φ E ?) "_ H◁ Htl HΦ". 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 & 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.
@@ -198,11 +198,11 @@ Section typing.
     consumes ty (λ ν, ν ◁ own q ty)%P
              (λ ν, ν ◁ own q (Π(replicate ty.(ty_size) uninit)))%P.
   Proof.
-    iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". iApply (has_type_wp with "[- $H◁]").
-    iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    iIntros (ν tid Φ E ?) "_ H◁ Htl HΦ". 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 & 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†".
@@ -219,12 +219,12 @@ Section typing.
                 (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
     iIntros (? ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) Htl HΦ".
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    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 H↦]". iDestruct "Heq" as %[=->].
     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.
@@ -237,14 +237,14 @@ Section typing.
                 (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
     iIntros (? ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) Htl HΦ".
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    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.
@@ -268,7 +268,7 @@ Section typing.
                (λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
     iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
+    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 H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
     iMod (borrow_acc_strong with "LFT H↦ Htok") as "[H↦ Hclose']". done.
@@ -288,17 +288,16 @@ Section typing.
                (λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
     iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑ & Htok) & $)". wp_bind ν.
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
+    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 #H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
     iDestruct "H↦" as (vl) "[H↦b Hown]".
-    iMod (frac_borrow_acc with "LFT [] H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
-    { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
+    iMod (frac_borrow_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     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'".
@@ -312,21 +311,25 @@ Section typing.
                (λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
   Proof.
     iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
+    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 H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
     iMod (borrow_exists with "LFT H↦") as (vl) "Hbor". done.
     iMod (borrow_split with "LFT Hbor") as "[H↦ Hbor]". done.
     iMod (borrow_exists with "LFT Hbor") as (l') "Hbor". done.
     iMod (borrow_split with "LFT Hbor") as "[Heq Hbor]". done.
-    iMod (borrow_unnest with "LFT Hbor") as "Hbor". done.
     iMod (borrow_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
     iMod (borrow_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
-    rewrite heap_mapsto_vec_singleton. wp_read.
-    iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
-    iMod ("Hclose" with "Htok") as "$". iFrame "#".
-    iMod "Hbor". iExists _. iSplitR. done. iApply (borrow_shorten with "[] Hbor").
-    iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl.
+    rewrite heap_mapsto_vec_singleton.
+    iApply (wp_strong_mono ⊤ ⊤ _ (λ v, _ ∗ ⌜v = #l'⌝ ∗ l ↦#l')%I). done.
+    iSplitR "Hbor H↦"; last first.
+    - iApply (wp_frame_step_l _ (⊤ ∖ ↑lftN) with "[-]"); try done; last first.
+      iSplitL "Hbor". by iApply (borrow_unnest with "LFT Hbor"). wp_read. auto.
+    - iIntros (v) "(Hbor & % & H↦)". subst.
+      iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
+      iMod ("Hclose" with "Htok") as "$". iFrame "#".
+      iExists _. iSplitR. done. iApply (borrow_shorten with "[] Hbor").
+      iApply (lft_incl_lb with "H⊑2"). iApply lft_incl_refl.
   Qed.
 
   Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
@@ -335,21 +338,20 @@ Section typing.
                (λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
   Proof.
     iIntros (tid) "!#(#HEAP & #LFT & (H◁ & #H⊑1 & Htok & #H⊑2) & $)". wp_bind ν.
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
+    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 %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
     iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
-    iMod (frac_borrow_acc with "LFT [] H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
-    { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
-    iAssert (κ' ⊑ κ'' ⋅ κ') as "#H⊑3".
-    { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
+    iMod (frac_borrow_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+    iAssert (κ' ⊑ κ'' ⋅ κ')%I as "#H⊑3".
+    { iApply (lft_incl_lb with "H⊑2 []"). iApply lft_incl_refl. }
     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);
-        last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
+      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".
       iMod ("Hclose'" with "[$H↦]") as "Htok'".
@@ -358,20 +360,19 @@ Section typing.
   Qed.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
-    ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
-      lft_ctx ⊢ ρ1 ν tid -∗
+    ∀ ν tid Φ E, mgmtE ∪ (↑lrustN) ⊆ E →
+      lft_ctx -∗ ρ1 ν tid -∗
       (∀ (l:loc) 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 {{ Φ }}.
+         (⌜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 {{ Φ }}.
 
   Lemma update_strong ty1 ty2 q:
     ty1.(ty_size) = ty2.(ty_size) →
     update ty1 (λ ν, ν ◁ own q ty2)%P (λ ν, ν ◁ own q ty1)%P.
   Proof.
-    iIntros (Hsz ν tid Φ E ?) "_ H◁ HΦ". iApply (has_type_wp with "[- $H◁]").
-    iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    iIntros (Hsz ν tid Φ E ?) "_ H◁ HΦ". 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 & H↦ & >H†)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%".
@@ -384,7 +385,7 @@ Section typing.
               (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
   Proof.
     iIntros (ν tid Φ E ?) "#LFT (H◁ & #H⊑ & Htok) HΦ".
-    iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
+    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 & H↦)". iDestruct "Heq" as %[=->].
     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.
@@ -401,7 +402,7 @@ Section typing.
     iIntros (Hsz Hupd tid) "!#(#HEAP & #LFT & [Hρ1 H◁] & $)". wp_bind ν1.
     iApply (Hupd with "LFT Hρ1"). done. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
     rewrite ->Hsz in *. destruct vl as [|v[|]]; try done.
-    wp_bind ν2. iApply (has_type_wp with "[- $H◁]"). iIntros (v') "[% H◁]!>".
+    wp_bind ν2. iApply (has_type_wp with "H◁"). iIntros (v') "% H◁!>".
     rewrite heap_mapsto_vec_singleton. wp_write.
     rewrite -heap_mapsto_vec_singleton has_type_value. iApply "Hupd". by iFrame.
   Qed.
@@ -450,7 +451,7 @@ Section typing.
     typed_program (ρ ∗ ν ◁ bool) (if: ν then e1 else e2).
   Proof.
     iIntros (He1 He2 tid) "!#(#HEAP & #LFT & [Hρ H◁] & Htl)".
-    wp_bind ν. iApply has_type_wp. iFrame. iIntros (v) "[% H◁]!>".
+    wp_bind ν. iApply (has_type_wp with "H◁"). iIntros (v) "% H◁!>".
     rewrite has_type_value. iDestruct "H◁" as (b) "Heq". iDestruct "Heq" as %[= ->].
     wp_if. destruct b; iNext. iApply He1; iFrame "∗#". iApply He2; iFrame "∗#".
   Qed.