diff --git a/iris b/iris
index f24fd7c35eb4e29c5fccb47200a22b7087fbcb64..36c5a84241841fadffaee32c710680b3c0d88eb0 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit f24fd7c35eb4e29c5fccb47200a22b7087fbcb64
+Subproject commit 36c5a84241841fadffaee32c710680b3c0d88eb0
diff --git a/theories/frac_borrow.v b/theories/frac_borrow.v
index 5d6959934113828a5f9c03e98c184ee0090445fc..9f1535a5adbd618a1b1b4bc860344fedd1863e31 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.
 
@@ -18,7 +19,7 @@ Section frac_borrow.
   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 φ E κ :
     ↑lftN ⊆ E → lft_ctx ⊢ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
@@ -29,10 +30,10 @@ Section frac_borrow.
       { 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.
@@ -50,54 +51,61 @@ Section frac_borrow.
       iApply fupd_intro_mask. set_solver. done.
   Qed.
 
-  Lemma frac_borrow_acc 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.[κ]).
+    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_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -∗ &frac{κ}φ.
+  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{κ}Φ.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame.
     iApply lft_incl_trans. iFrame.
@@ -108,9 +116,8 @@ Section frac_borrow.
   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 5e4a0ba95b7c8756174f5c68ee9d946ec0524a26..58d0bf7caea1be6bb75c2b7b596b686f261a23bf 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.
@@ -118,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.
   Proof.
     destruct (decide (v1 = v2)) as [->|].
-    { by rewrite heap_mapsto_op_eq pure_True // 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 /=.
@@ -159,12 +172,6 @@ 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.
@@ -176,7 +183,7 @@ Section heap.
       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 Σ) :
@@ -189,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,
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/lifetime.v b/theories/lifetime.v
index bbc61eef5047531af2275dd194e8d7b84c94fa01..a63ba53d5829288895bf69a20c5f9615519bf887 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Import csum auth frac gmap.
 From iris.base_logic.lib Require Export fancy_updates invariants namespaces.
+From iris.base_logic.lib Require Export fractional.
 From iris.proofmode Require Import tactics.
 
 Definition lftN := nroot .@ "lft".
@@ -72,10 +73,23 @@ Section lft.
 
   Axiom lft_ctx_alloc : True ={∅}=∗ lft_ctx.
 
-  (*** PersitentP, TimelessP and Proper instances  *)
+  (*** PersitentP, TimelessP, Proper and Fractional instances  *)
 
   Global Instance lft_own_timeless q κ : TimelessP q.[κ].
   Proof. unfold lft_own. apply _. Qed.
+  Global Instance lft_own_fractional κ : Fractional (λ q, q.[κ])%I.
+  Proof.
+    intros p q. rewrite /lft_own -own_op -auth_frag_op.
+    f_equiv. constructor. done. simpl. intros Λ.
+    rewrite lookup_op !lookup_fmap !lookup_omap. apply reflexive_eq.
+    case: (κ !! Λ)=>[[|a]|]//=. rewrite -Some_op Cinl_op. repeat f_equal.
+    induction a as [|a IH]. done.
+    rewrite /= IH /op /cmra_op /= /frac_op !assoc. f_equal.
+    rewrite -!assoc. f_equal. apply (comm _).
+  Qed.
+  Global Instance lft_own_as_fractional κ q :
+    AsFractional q.[κ] (λ q, q.[κ])%I q.
+  Proof. done. Qed.
 
   Global Instance lft_dead_persistent κ : PersistentP [†κ].
   Proof. unfold lft_dead. apply _. Qed.
@@ -120,17 +134,6 @@ Section lft.
       (iRight + iLeft); iExists Λ; iIntros "{$Hown}!%"; by eauto.
   Qed.
 
-  Lemma lft_own_frac_op κ q q':
-       (q + q').[κ] ⊣⊢ q.[κ] ∗ q'.[κ].
-  Proof.
-    rewrite /lft_own -own_op -auth_frag_op. f_equiv. constructor. done. simpl.
-    intros Λ. rewrite lookup_op !lookup_fmap !lookup_omap. apply reflexive_eq.
-    case: (κ !! Λ)=>[[|a]|]//=. rewrite -Some_op Cinl_op. repeat f_equal.
-    induction a as [|a IH]. done.
-    rewrite /= IH /op /cmra_op /= /frac_op !assoc. f_equal.
-    rewrite -!assoc. f_equal. apply (comm _).
-  Qed.
-
   Axiom lft_create :
     ∀ `(↑lftN ⊆ E),
       lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
@@ -167,7 +170,7 @@ Section lft.
     ∀ `(↑lftN ⊆ E) κ κ' P, κ ≼ κ' →
       lft_ctx ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
   Axiom borrow_unnest :
-    ∀ `(↑lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E}▷=∗ &{κ ⋅ κ'}P.
+    ∀ `(↑lftN ⊆ E) κ κ' P, lft_ctx ⊢ &{κ'}&{κ}P ={E, E∖↑lftN}▷=∗ &{κ ⋅ κ'}P.
 
   (*** Derived lemmas  *)
 
@@ -193,29 +196,6 @@ Section lft.
     iIntros "HΛ". iDestruct "HΛ" as (Λ) "[% _]". naive_solver.
   Qed.
 
-  Lemma lft_own_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ∗ (q/2).[κ].
-  Proof. by rewrite -lft_own_frac_op Qp_div_2. Qed.
-
-  Global Instance into_and_lft_own_half κ q :
-    IntoAnd false q.[κ] (q/2).[κ] (q/2).[κ] | 100.
-  Proof. by rewrite /IntoAnd lft_own_split. Qed.
-
-  Global Instance from_sep_lft_own_half κ q :
-    FromSep q.[κ] (q/2).[κ] (q/2).[κ] | 100.
-  Proof. by rewrite /FromSep -lft_own_split. Qed.
-
-  Global Instance frame_lft_own_half κ q :
-    Frame (q/2).[κ] q.[κ] (q/2).[κ] | 100.
-  Proof. by rewrite /Frame -lft_own_split. Qed.
-
-  Global Instance into_and_lft_own_frac κ q1 q2 :
-    IntoAnd false (q1+q2).[κ] q1.[κ] q2.[κ].
-  Proof. by rewrite /IntoAnd lft_own_frac_op. Qed.
-
-  Global Instance from_sep_lft_own_frac κ q1 q2 :
-    FromSep (q1+q2).[κ] q1.[κ] q2.[κ].
-  Proof. by rewrite /FromSep -lft_own_frac_op. Qed.
-
   Global Instance into_and_lft_own κ1 κ2 q :
     IntoAnd false q.[κ1⋅κ2] q.[κ1] q.[κ2].
   Proof. by rewrite /IntoAnd lft_own_op. Qed.
@@ -327,10 +307,9 @@ Section incl.
       iMod ("H1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
       iMod ("H2" with "*Hκ'2") as (q'') "[Hκ'' Hclose'']".
       destruct (Qp_lower_bound q' q'') as (qq & q'0 & q''0 & -> & ->).
-      iExists qq. rewrite -lft_own_op !lft_own_frac_op.
+      iExists qq. rewrite -lft_own_op.
       iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
-      iIntros "!>[Hκ'0 Hκ''0]".
-      iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
+      iIntros "!>[Hκ'0 Hκ''0]". iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
       by iMod ("Hclose''" with "[$Hκ'' $Hκ''0]") as "$".
     - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
   Qed.
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index 93eebced650654f2a41012465ea82cbe38dccf1b..944f9b06fcaa6a59dd8b6bb3a8cf327a0714de43 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -93,9 +93,7 @@ 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.
diff --git a/theories/proofmode.v b/theories/proofmode.v
index 7c1cde572271bba6a50706ece3235c540fba019d..dbd10fe695c5eca23088bfa4f57ee6822605890d 100644
--- a/theories/proofmode.v
+++ b/theories/proofmode.v
@@ -12,14 +12,6 @@ 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) → ↑heapN ⊆ E → 0 < n →
   IntoLaterEnvs Δ Δ' →
diff --git a/theories/type.v b/theories/type.v
index abbe4b63cca0514469476e4d44287e2356b8d9db..9a4880825c13cc48165eab92a708b05c54a7fc1e 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -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.
@@ -213,7 +209,7 @@ Section types.
        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.
@@ -232,16 +228,19 @@ Section types.
     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".
@@ -325,7 +324,7 @@ 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.
+    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 ">%".
@@ -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 "$".
diff --git a/theories/typing.v b/theories/typing.v
index d7f653f80e211bf4527722798dc9d92c50eae018..a50ed406cd787f69e12f90c6bab298e7565650ba 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -292,8 +292,7 @@ Section typing.
     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.
@@ -319,14 +318,18 @@ Section typing.
     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. iSplit. done. iApply lft_incl_refl.
   Qed.
 
   Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
@@ -339,8 +342,7 @@ Section typing.
     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. }
+    iMod (frac_borrow_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
     iAssert (κ' ⊑ κ'' ⋅ κ') as "#H⊑3".
     { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
     iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
@@ -349,7 +351,7 @@ Section typing.
     - 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).
+        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'".