diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
index 3c74848b7921d164cd994ccc18112a09ca7ad400..972f29d90efd20306a8b9b46d9f9f82209331485 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/accessors.v
@@ -1,34 +1,235 @@
-From lrust.lifetime Require Export definitions.
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.base_logic Require Import big_op.
+From iris.base_logic.lib Require Import boxes.
+From lrust.lifetime Require Export primitive rebor.
 
 Section accessors.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
+(* Helper internal lemmas *)
+
+Lemma bor_open_internal E P i Pb q :
+  ↑borN ⊆ E →
+  slice borN (i.2) P -∗ ▷ lft_bor_alive (i.1) Pb -∗
+  idx_bor_own 1%Qp i -∗ (q).[i.1] ={E}=∗
+    ▷ lft_bor_alive (i.1) Pb ∗
+    own_bor (i.1) (◯ {[i.2 := (1%Qp, DecAgree (Bor_open q))]}) ∗ ▷ P.
+Proof.
+  iIntros (?) "Hslice Halive Hbor Htok". unfold lft_bor_alive, idx_bor_own.
+  iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
+  iDestruct (own_bor_valid_2 with "Hown Hbor")
+    as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+  iMod (box_empty with "Hslice Hbox") as "[$ Hbox]".
+    solve_ndisj. by rewrite lookup_fmap EQB.
+  rewrite -(fmap_insert bor_filled _ _ (Bor_open q)).
+  iMod (own_bor_update_2 with "Hown Hbor") as "Hbor". apply auth_update.
+  { eapply singleton_local_update. by rewrite lookup_fmap EQB.
+    by apply (exclusive_local_update _ (1%Qp, DecAgree (Bor_open q))). }
+  rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
+  iExists _. iFrame "∗".
+  rewrite -insert_delete big_sepM_insert ?lookup_delete // big_sepM_delete /=; last done.
+  iDestruct "HB" as "[_ $]". auto.
+Qed.
+
+Lemma bor_close_internal E P i Pb q :
+  ↑borN ⊆ E →
+  slice borN (i.2) P -∗ ▷ lft_bor_alive (i.1) Pb -∗
+  own_bor (i.1) (◯ {[i.2 := (1%Qp, DecAgree (Bor_open q))]}) -∗ ▷ P ={E}=∗
+    ▷ lft_bor_alive (i.1) Pb ∗ idx_bor_own 1%Qp i ∗ (q).[i.1].
+Proof.
+  iIntros (?) "Hslice Halive Hbor HP". unfold lft_bor_alive, idx_bor_own.
+  iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
+  iDestruct (own_bor_valid_2 with "Hown Hbor")
+    as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+  iMod (box_fill with "Hslice HP Hbox") as "Hbox".
+    solve_ndisj. by rewrite lookup_fmap EQB.
+  rewrite -(fmap_insert bor_filled _ _ Bor_in).
+  iMod (own_bor_update_2 with "Hown Hbor") as "Hbor". apply auth_update.
+  { eapply singleton_local_update. by rewrite lookup_fmap EQB.
+    by apply (exclusive_local_update _ (1%Qp, DecAgree Bor_in)). }
+  rewrite own_bor_op -fmap_insert. iDestruct "Hbor" as "[Hown $]".
+  rewrite big_sepM_delete //. simpl. iDestruct "HB" as "[>$ HB]".
+  iExists _. iFrame "Hbox Hown".
+  rewrite -insert_delete big_sepM_insert ?lookup_delete //. simpl. by iFrame.
+Qed.
+
+Lemma bor_acc_internal E P i Pb q :
+  ↑borN ⊆ E →
+  slice borN (i.2) P -∗ ▷ lft_bor_alive (i.1) Pb -∗ idx_bor_own q%Qp i ={E}=∗
+    ▷ P ∗ (▷ P ={E}=∗ ▷ lft_bor_alive (i.1) Pb ∗ idx_bor_own q%Qp i).
+Proof.
+  iIntros (?) "#Hslice Halive Hbor". unfold lft_bor_alive, idx_bor_own.
+  iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
+  iDestruct (own_bor_valid_2 with "Hown Hbor")
+    as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+  iMod (box_empty with "Hslice Hbox") as "[$ Hbox]".
+    solve_ndisj. by rewrite lookup_fmap EQB.
+  iIntros "!>HP{$Hbor}". iMod (box_fill with "Hslice HP Hbox") as "Hbox".
+    done. by rewrite lookup_insert.
+  iExists _. iFrame. rewrite insert_insert insert_id // lookup_fmap EQB //.
+Qed.
+
+Lemma create_dead A κ:
+  lft_dead_in A κ →
+  own_alft_auth A ==∗ own_alft_auth A ∗ [†κ].
+Proof.
+  iIntros ((Λ & HΛκ & EQΛ)) "HA". unfold own_alft_auth, lft_dead.
+  iMod (own_update _ ((● to_alftUR A)) with "HA") as "HA".
+  { eapply (auth_update_alloc _ _ ({[Λ := Cinr ()]}⋅∅)), op_local_update_discrete=>HA Λ'.
+    specialize (HA Λ'). revert HA.
+    rewrite lookup_op lookup_fmap. destruct (decide (Λ = Λ')) as [<-|].
+    - by rewrite lookup_singleton EQΛ.
+    - rewrite lookup_singleton_ne //. by destruct (to_lft_stateR <$> A !! Λ'). }
+  rewrite right_id. iDestruct "HA" as "[HA HΛ]". iSplitL "HA"; last (iExists _; by iFrame).
+  assert ({[Λ := Cinr ()]} ⋅ to_alftUR A ≡ to_alftUR A) as ->; last done.
+  intros Λ'. rewrite lookup_op. destruct (decide (Λ = Λ')) as [<-|].
+  - by rewrite lookup_singleton lookup_fmap EQΛ.
+  - rewrite lookup_singleton_ne //. by case: (to_alftUR A !! Λ').
+Qed.
+
+Lemma add_vs Pb Pb' P Q Pi κ :
+  ▷ ▷ (Pb ≡ (P ∗ Pb')) -∗ ▷ lft_vs κ Pb Pi -∗ ▷ (▷ Q -∗ [†κ] ={⊤∖↑lftN}=∗ ▷ P) -∗
+  ▷ lft_vs κ (Q ∗ Pb') Pi.
+Proof.
+  iIntros "#HEQ Hvs HvsQ". iNext. rewrite !lft_vs_unfold.
+  iDestruct "Hvs" as (n) "[Hcnt Hvs]". iExists n.
+  iIntros "{$Hcnt}*Hinv[HQ HPb] #H†". iApply fupd_trans.
+  iApply fupd_mask_mono; last iMod ("HvsQ" with "HQ H†") as "HP". solve_ndisj.
+  iModIntro. iAssert (â–· Pb)%I with "[HPb HP]" as "HPb".
+  { iNext. iRewrite "HEQ". iFrame. }
+  iApply ("Hvs" with "* Hinv HPb H†").
+Qed.
+
+(** Indexed borrow *)
+
+Lemma idx_bor_acc E q κ i P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
+            ▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ]).
+Proof.
+  unfold idx_bor. iIntros (HE) "#LFT [#Hle #Hs] Hbor Htok".
+  iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". solve_ndisj.
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
+  iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
+  rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
+          /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
+  iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
+  - iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
+    iMod (bor_open_internal with "Hs Halive Hbor Htok") as "(Halive & Hf & $)".
+      solve_ndisj.
+    iMod ("Hclose'" with "[-Hf Hclose]") as "_".
+    { iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
+      iLeft. iFrame "%". iExists _, _. iFrame. }
+    iIntros "!>HP". clear -HE.
+    iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
+    iDestruct (own_bor_auth with "HI Hf") as %Hκ'.
+    rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
+            /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in /lft_bor_dead.
+    iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >Hdead_in]] Hclose'']".
+    + rewrite lft_inv_alive_unfold.
+      iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
+      iMod (bor_close_internal with "Hs Halive Hf HP") as "(Halive & $ & Htok)".
+        solve_ndisj.
+      iMod ("Hclose'" with "[-Htok Hclose]") as "_"; last by iApply "Hclose".
+      iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
+      iLeft. iFrame "%". iExists _, _. iFrame.
+    + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
+      iDestruct (own_bor_valid_2 with "Hinv Hf")
+        as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
+      by destruct INCL as [[=]|(? & ? & [=<-] &
+        [[_<-]%lookup_to_gmap_Some [[_[=]]|[]%(exclusive_included _)]])].
+  - iMod (create_dead with "HA") as "[_ H†]". done.
+    iDestruct (lft_tok_dead with "Htok H†") as "[]".
+Qed.
+
+Lemma idx_bor_atomic_acc E q κ i P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ,i}P -∗ idx_bor_own q i ={E,E∖↑lftN}=∗
+              ▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_bor_own q i) ∨
+              ([†κ] ∗ |={E∖↑lftN,E}=> idx_bor_own q i).
+Proof.
+  unfold idx_bor. iIntros (HE) "#LFT [#Hle #Hs] Hbor".
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
+  iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
+  rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
+          /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
+  iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
+  - iLeft. iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
+    iMod (bor_acc_internal with "Hs Halive Hbor") as "($ & Hf)". solve_ndisj.
+    iMod fupd_intro_mask' as "Hclose"; last iIntros "!>HP". solve_ndisj.
+    iMod "Hclose" as "_". iMod ("Hf" with "HP") as "[Hinv $]". iApply "Hclose'".
+    iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". iLeft.
+    iFrame "%". iExists _, _. iFrame.
+  - iRight. iMod (create_dead with "HA") as "[HA #H†]". done.
+    iMod ("Hclose'" with "[-Hbor]") as "_".
+    + iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
+    + iMod (lft_incl_dead with "Hle H†"). done. iFrame.
+      iApply fupd_intro_mask'. solve_ndisj.
+Qed.
+
 (** Basic borrows  *)
+
 Lemma bor_acc_strong E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
-    ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
-Proof. Admitted.
+    ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ] ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
+Proof.
+  unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
+  iDestruct "Hbor" as (i) "(#Hle & Hbor & #Hs)".
+  iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". solve_ndisj.
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
+  iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
+  rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
+          /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
+  iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
+  - iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
+    iMod (bor_open_internal with "Hs Halive Hbor Htok") as "(Halive & Hbor & $)".
+      solve_ndisj.
+    iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
+    { iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
+      iLeft. iFrame "%". iExists _, _. iFrame. }
+    iIntros "!>*HQ HvsQ". clear -HE.
+    iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
+    iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
+    rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
+            /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in /lft_bor_dead.
+    iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >Hdead_in]] Hclose'']".
+    + rewrite lft_inv_alive_unfold /lft_bor_alive.
+      iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
+      iDestruct "Halive" as (B) "(Hbox & >Hown & HB)".
+      iDestruct (own_bor_valid_2 with "Hown Hbor")
+        as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+      iMod (box_delete_empty with "Hs Hbox") as (Pb') "[EQ Hbox]".
+        solve_ndisj. by rewrite lookup_fmap EQB.
+      iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
+      { iNext. iIntros "HQ H†". iApply ("HvsQ" with "HQ"). admit. }
+      iMod (box_insert_empty with "Hbox") as (γ) "(% & Hs' & Hbox)".
+      admit.
+    + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
+      iDestruct (own_bor_valid_2 with "Hinv Hbor")
+        as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
+      by destruct INCL as [[=]|(? & ? & [=<-] &
+        [[_<-]%lookup_to_gmap_Some [[_[=]]|[]%(exclusive_included _)]])].
+  - iMod (create_dead with "HA") as "[_ H†]". done.
+    iDestruct (lft_tok_dead with "Htok H†") as "[]".
+Admitted.
+
 Lemma bor_acc_atomic_strong E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-    (▷ P ∗ ∀ Q, ▷ Q ∗ ▷ ([†κ] -∗ ▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+    (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ] ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
     [†κ] ∗ |={E∖↑lftN,E}=> True.
 Proof. Admitted.
 
-(** Indexed borrow *)
-Lemma idx_bor_acc E q κ i P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ idx_bor κ i P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
-            ▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ]).
-Proof. Admitted.
-
-Lemma idx_bor_atomic_acc E q κ i P :
+Lemma bor_acc E q κ P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ idx_bor κ i P -∗ idx_bor_own q i ={E,E∖↑lftN}=∗
-              ▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_bor_own q i) ∨
-              [†κ] ∗ (|={E∖↑lftN,E}=> idx_bor_own q i).
-Proof. Admitted.
+  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
+Proof.
+  iIntros (?) "#LFT HP Htok".
+  iMod (bor_acc_strong with "LFT HP Htok") as "[HP Hclose]"; first done.
+  iIntros "!> {$HP} HP". iApply ("Hclose" with "HP"). by iIntros "!>$_".
+Qed.
 
 End accessors.
\ No newline at end of file
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 263a0af2d56d69a4f14e71e580b22201d4d61221..de70d2be9c63d2f2165e2ceeede556d71014aa51 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -6,14 +6,6 @@ Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
 (*** Derived lemmas  *)
-Lemma bor_acc E q κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
-Proof.
-  iIntros (?) "#LFT HP Htok".
-  iMod (bor_acc_strong with "LFT HP Htok") as "[HP Hclose]"; first done.
-  iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>_$".
-Qed.
 
 Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
   ↑lftN ⊆ E →
@@ -22,7 +14,7 @@ Proof.
   iIntros (?) "#LFT Hb".
   iMod (bor_acc_atomic_strong with "LFT Hb") as "[[HΦ Hclose]|[H† Hclose]]"; first done.
   - iDestruct "HΦ" as (x) "HΦ". iExists x.
-    iApply "Hclose". iIntros "{$HΦ} !> _ ?"; eauto.
+    iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
   - iMod "Hclose" as "_". iExists inhabitant. by iApply (bor_fake with "LFT").
 Qed.
 
@@ -34,29 +26,32 @@ Proof.
   iMod (bor_exists with "LFT H") as ([]) "H"; auto.
 Qed.
 
-Lemma bor_persistent P `{!PersistentP P} E κ q :
+Lemma bor_later E κ P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
+  lft_ctx -∗ &{κ}(▷ P) ={E,E∖↑lftN}▷=∗ &{κ}P.
 Proof.
-  iIntros (?) "#LFT Hb Htok".
-  iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
-  by iMod ("Hob" with "HP") as "[_$]".
+  iIntros (?) "#LFT Hb".
+  iMod (bor_acc_atomic_strong with "LFT Hb") as "[[HP Hclose]|[H† Hclose]]"; first done.
+  - iModIntro. iNext. iApply ("Hclose" with "* HP"). by iIntros "!>$_".
+  - iIntros "!>!>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
 Qed.
 
-Lemma lft_incl_acc E κ κ' q :
+Lemma bor_later_tok E q κ P :
   ↑lftN ⊆ E →
-  κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+  lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].
 Proof.
-  rewrite /lft_incl.
-  iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
-  iMod ("H" with "* Hq") as (q') "[Hq' Hclose]". iExists q'.
-  iIntros "{$Hq'} !> Hq". iApply fupd_mask_mono; first done. by iApply "Hclose".
+  iIntros (?) "#LFT Hb Htok".
+  iMod (bor_acc_strong with "LFT Hb Htok") as "[HP Hclose]"; first done.
+  iModIntro. iNext. iApply ("Hclose" with "* HP"). by iIntros "!>$_".
 Qed.
 
-Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
+Lemma bor_persistent P `{!PersistentP P} E κ q :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
 Proof.
-  rewrite /lft_incl.
-  iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
+  iIntros (?) "#LFT Hb Htok".
+  iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
+  by iMod ("Hob" with "HP") as "[_$]".
 Qed.
 
 Lemma lft_incl_static κ : (κ ⊑ static)%I.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index ea78aee6e7e0203e22b7ec9db6ea273f65f1fa3c..475dfca4a3fc1f5d196cd6b0a251cf88eb493b95 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -26,13 +26,13 @@ Section frac_bor.
   Proof.
     iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
     iMod (bor_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
-    - iMod ("Hclose" with "*[-]") as "Hφ"; last first.
+    - iMod ("Hclose" with "*[-] []") as "Hφ"; last first.
       { iExists γ, κ. iSplitR; last by iApply (bor_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.
-      iDestruct "Hκ" as (q'') "[_ Hκ]".
-      iDestruct (lft_tok_dead with "Hκ H†") as "[]".
+      { iIntros "!>HΦ H†!>". iNext. iDestruct "HΦ" as (q') "(HΦ & _ & [%|Hκ])". by subst.
+        iDestruct "Hκ" as (q'') "[_ Hκ]".
+        iDestruct (lft_tok_dead with "Hκ H†") as "[]". }
+      iExists 1%Qp. iFrame. eauto.
     - iMod ("Hclose" with "*") as "HΦ"; last first.
       iExists γ, κ. iSplitR. by iApply lft_incl_refl.
       iMod (bor_fake with "LFT H†"). done. by iApply bor_share.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 33e0e6f32377393a4b3c749ff405036ae802b817..83ccf906a54bc3f19125efd8feed72795d6c932d 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -9,8 +9,8 @@ Section primitive.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-Lemma to_borUR_included (B : gmap slice_name bor_state) i s :
-  {[i := (1%Qp, DecAgree s)]} ≼ to_borUR B → B !! i = Some s.
+Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
+  {[i := (q%Qp, DecAgree s)]} ≼ to_borUR B → B !! i = Some s.
 Proof.
   rewrite singleton_included=> -[qs [/leibniz_equiv_iff]].
   rewrite lookup_fmap fmap_Some=> -[s' [? ->]].
@@ -208,7 +208,7 @@ Proof.
 Qed.
 
 (** Basic rules about lifetimes  *)
-Lemma lft_tok_op q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
+Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
 Proof. by rewrite /lft_tok -big_sepMS_union. Qed.
 
 Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ∪ κ2].
@@ -253,8 +253,8 @@ Proof. done. Qed.
 Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
 Proof.
   iIntros (->%gmultiset_union_difference) "!#". iSplitR.
-  - iIntros (q). rewrite <-lft_tok_op. iIntros "[H Hf]". iExists q. iFrame.
-    rewrite <-lft_tok_op. by iIntros "!>{$Hf}$".
+  - iIntros (q). rewrite <-lft_tok_sep. iIntros "[H Hf]". iExists q. iFrame.
+    rewrite <-lft_tok_sep. by iIntros "!>{$Hf}$".
   - iIntros "? !>". iApply lft_dead_or. auto.
 Qed.
 
@@ -279,7 +279,7 @@ Proof.
     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_tok_op.
+    iExists qq. rewrite -lft_tok_sep.
     iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
     iIntros "!>[Hκ'0 Hκ''0]".
     iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
@@ -287,4 +287,20 @@ Proof.
   - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
 Qed.
 
+Lemma lft_incl_acc E κ κ' q :
+  ↑lftN ⊆ E →
+  κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+Proof.
+  rewrite /lft_incl.
+  iIntros (?) "#[H _] Hq". iApply fupd_mask_mono; first done.
+  iMod ("H" with "* Hq") as (q') "[Hq' Hclose]". iExists q'.
+  iIntros "{$Hq'} !> Hq". iApply fupd_mask_mono; first done. by iApply "Hclose".
+Qed.
+
+Lemma lft_incl_dead E κ κ' : ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
+Proof.
+  rewrite /lft_incl.
+  iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
+Qed.
+
 End primitive.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 2f7e5ea823c90f662aa99389cc3241c7f159185b..8f3bdd31ca2fa2e440b8322bb3162b197789f1aa 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -180,13 +180,11 @@ Section types.
     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".
+    - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hb". set_solver.
       { rewrite bor_unfold_idx. iExists i. eauto. }
-      iMod (bor_acc_strong with "LFT Hb Htok") as "[Hown Hclose']". set_solver.
-      iIntros "!>". iNext.
-      iMod ("Hclose'" with "*[Hown]") as "[Hb Htok]". iFrame. by iIntros "!>?$".
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done.
-      iMod ("Hclose" with "[]") as "_"; by eauto.
+      iIntros "!>". iNext. iMod "Hb" as "[Hb Htok]".
+      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; try done.
+      iApply "Hclose". eauto.
     - iIntros "!>". iNext. iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
   Next Obligation.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index f9d4063712724f535ec6bfff248fbfbcfb1c208e..8a0384d629d339c6e1208a78c26891a6c5cb411e 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -276,11 +276,12 @@ Section typing.
     iMod (bor_acc_strong with "LFT H↦ Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
     subst. rewrite heap_mapsto_vec_singleton. wp_read.
-    iMod ("Hclose'" with "*[H↦ Hown H†]") as "[Hbor Htok]"; last first.
+    iMod ("Hclose'" with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
     - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
       iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
       iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
-    - iIntros "{$H↦ $H† $Hown}!>_(?&?&?)!>". iNext. iExists _.
+    - iFrame "H↦ H† Hown".
+    - iIntros "!>(?&?&?)_!>". iNext. iExists _.
       rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
   Qed.