diff --git a/_CoqProject b/_CoqProject
index 99d284ab9a620e7face66e98e0d56c74f7b4b112..5ef0e7675ba981ad88b422b8d7971f4476625f59 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,8 +5,9 @@ theories/lifetime/derived.v
 theories/lifetime/creation.v
 theories/lifetime/primitive.v
 theories/lifetime/accessors.v
+theories/lifetime/raw_reborrow.v
 theories/lifetime/borrow.v
-theories/lifetime/rebor.v
+theories/lifetime/reborrow.v
 theories/lifetime/shr_borrow.v
 theories/lifetime/frac_borrow.v
 theories/lifetime/tl_borrow.v
diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
index cf8c06d846ca801ff3f80c5946cf5dfa3d62ef3a..ae90412a50e220dced388e224f6e6b46a4d5ec25 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/accessors.v
@@ -1,15 +1,14 @@
+From lrust.lifetime Require Export primitive.
 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 borrow.
 
 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 -∗
@@ -87,7 +86,6 @@ Proof.
 Qed.
 
 (** Indexed borrow *)
-
 Lemma idx_bor_acc E q κ i P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index c4e5f040eb40bf8da48a19b218d4feee5cbc2240..04c1c297783d9388089c9e7fc51669659ede0914 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -1,4 +1,5 @@
-From lrust.lifetime Require Export primitive creation rebor.
+From lrust.lifetime Require Export primitive creation.
+From lrust.lifetime Require Export raw_reborrow.
 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.
@@ -8,47 +9,12 @@ Section borrow.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
-Proof.
-  rewrite /bor /raw_bor /idx_bor /bor_idx. iProof; iSplit.
-  - iIntros "H". iDestruct "H" as (κ') "[? Hraw]". iDestruct "Hraw" as (s) "[??]".
-    iExists (κ', s). by iFrame.
-  - iIntros "H". iDestruct "H" as ([κ' s]) "[[??]?]". iExists κ'. iFrame.
-    iExists s. by iFrame.
-Qed.
-
-Lemma bor_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
-Proof.
-  unfold bor. iIntros "#Hκκ' H". iDestruct "H" as (i) "[#? ?]".
-  iExists i. iFrame. by iApply (lft_incl_trans with "Hκκ'").
-Qed.
-
-Lemma idx_bor_shorten κ κ' i P : κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
-Proof. unfold idx_bor. iIntros "#Hκκ' [#? $]". by iApply (lft_incl_trans with "Hκκ'"). Qed.
-
-Lemma bor_fake E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
-Proof.
-  iIntros (?) "#Hmgmt H†". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iMod (ilft_create _ _ κ with "HI HA Hinv") as (A' I') "(Hκ & HI & HA & Hinv)".
-  iDestruct "Hκ" as %Hκ. rewrite /lft_dead. iDestruct "H†" as (Λ) "[% #H†]".
-  iDestruct (own_alft_auth_agree A' Λ false with "HA H†") as %EQAΛ.
-  rewrite big_sepS_later big_sepS_elem_of_acc
-          ?elem_of_dom // /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in.
-  iDestruct "Hinv" as "[[[_ >%]|[Hinv >%]]Hclose']". naive_solver.
-  iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
-  iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
-  unfold bor. iExists κ. iFrame. rewrite -lft_incl_refl -big_sepS_later.
-  iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame. eauto.
-Qed.
-
 Lemma bor_create E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
 Proof.
   iIntros (HE) "#Hmgmt HP". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iMod (ilft_create _ _ κ with "HI HA Hinv") as (A' I') "(Hκ & HI & HA & Hinv)".
+  iMod (ilft_create _ _ κ with "HA HI Hinv") as (A' I') "(Hκ & HA & HI & Hinv)".
   iDestruct "Hκ" as %Hκ. iDestruct (@big_sepS_later with "Hinv") as "Hinv".
   iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose']".
   { by apply elem_of_dom. }
@@ -56,41 +22,32 @@ Proof.
   - rewrite {1}lft_inv_alive_unfold;
       iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
     rewrite /lft_bor_alive; iDestruct "Halive" as (B) "(HboxB & >HownB & HB)".
-    rewrite /lft_inh; iDestruct "Hinh" as (PE) "[>HownE HboxE]".
+    iMod (lft_inh_acc _ _ P with "Hinh") as "[Hinh Hinh_close]"; first solve_ndisj.
     iMod (slice_insert_full _ _ true with "HP HboxB")
       as (γB) "(HBlookup & HsliceB & HboxB)"; first by solve_ndisj.
     rewrite lookup_fmap. iDestruct "HBlookup" as %HBlookup.
-    iMod (slice_insert_empty _ _ true _ P with "HboxE")
-      as (γE) "(% & HsliceE & HboxE)".
-    rewrite -(fmap_insert bor_filled _ _ Bor_in) -to_gmap_union_singleton.
-    iMod (own_bor_update with "HownB") as "HownB".
+    rewrite -(fmap_insert bor_filled _ _ Bor_in).
+    iMod (own_bor_update with "HownB") as "[HB● HB◯]".
     { eapply auth_update_alloc,
-        (alloc_local_update _ _ γB (1%Qp, DecAgree Bor_in)); last done.
+        (alloc_singleton_local_update _ γB (1%Qp, DecAgree Bor_in)); last done.
       rewrite lookup_fmap. by destruct (B !! γB). }
-    iMod (own_inh_update with "HownE") as "HownE".
-    { by eapply auth_update_alloc, (gset_disj_alloc_empty_local_update _ {[γE]}),
-        disjoint_singleton_l, lookup_to_gmap_None. }
-    rewrite -fmap_insert own_bor_op own_inh_op insert_empty.
-    iDestruct "HownB" as "[HB● HB◯]". iDestruct "HownE" as "[HE● HE◯]".
-    iSpecialize ("Hclose'" with "[Hvs HboxE HboxB HB● HE● HB]").
+    rewrite -fmap_insert.
+    iSpecialize ("Hclose'" with "[Hvs Hinh HboxB HB● HB]").
     { iNext. rewrite /lft_inv. iLeft. iFrame "%".
       rewrite lft_inv_alive_unfold. iExists (P ∗ Pb)%I, (P ∗ Pi)%I.
-      iSplitL "HboxB HB● HB"; last iSplitL "Hvs".
-      - rewrite /lft_bor_alive.
-        iExists _. iFrame "HboxB HB●".
-        iApply @big_sepM_insert; first by destruct (B !! γB).
-        simpl. iFrame.
-      - rewrite !lft_vs_unfold. iDestruct "Hvs" as (n) "[Hcnt Hvs]".
-        iExists n. iFrame "Hcnt". iIntros (I'') "Hvsinv [$ HPb] H†".
-        iApply ("Hvs" $! I'' with "Hvsinv HPb H†").
-      - rewrite /lft_inh. iExists _. iFrame. }
+      iFrame "Hinh". iSplitL "HboxB HB● HB"; last by iApply lft_vs_frame.
+      rewrite /lft_bor_alive. iExists _. iFrame "HboxB HB●".
+      iApply @big_sepM_insert; first by destruct (B !! γB).
+      simpl. iFrame. }
     iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iExists _, _; iFrame|].
     iSplitL "HBâ—¯ HsliceB".
     + rewrite /bor /raw_bor /idx_bor_own. iExists κ; simpl.
       iModIntro. iSplit; first by iApply lft_incl_refl. iExists γB. by iFrame.
     + clear -HE. iIntros "!> H†".
       iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-      iDestruct (own_inh_auth with "HI HE◯") as %Hκ.
+      iAssert ⌜ is_Some (I !! κ) ⌝%I with "[#]" as %Hκ.
+      { iDestruct "Hinh_close" as "[H _]". by iApply "H". }
+      iDestruct "Hinh_close" as "[_ Hinh_close]".
       iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose']".
       { by apply elem_of_dom. }
       rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
@@ -98,22 +55,10 @@ Proof.
       rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >%]|[Hinv >%]]".
       { unfold lft_alive_in in *. naive_solver. }
       rewrite /lft_inv_dead; iDestruct "Hinv" as (Pinh) "(Hdead & >Hcnt & Hinh)".
-      rewrite /lft_inh; iDestruct "Hinh" as (ESlices) "[>Hinh Hbox]".
-      iDestruct (own_inh_valid_2 with "Hinh HEâ—¯")
-        as %[Hle%gset_disj_included _]%auth_valid_discrete_2.
-      rewrite <-elem_of_subseteq_singleton in Hle.
-      iMod (own_inh_update with "[HE◯ Hinh]") as "HE●"; [|iApply own_inh_op; by iFrame|].
-      { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
-      iMod (slice_delete_full _ _ true with "HsliceE Hbox")
-        as (Pinh') "($ & _ & Hbox)"; first by solve_ndisj.
-      { by rewrite lookup_to_gmap_Some. }
+      iMod ("Hinh_close" $! Pinh with "Hinh") as (Pinh') "(? & $ & ?)".
       iApply "Hclose". iExists A, I. iFrame. iNext. iApply "Hclose'".
       rewrite /lft_inv. iRight. iFrame "%".
       rewrite /lft_inv_dead. iExists Pinh'. iFrame.
-      rewrite /lft_inh. iExists _. iFrame.
-      rewrite {1}(union_difference_L {[γE]} ESlices); last set_solver.
-      rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None.
-      set_solver+.
   - iFrame "HP". iApply fupd_frame_r. iSplitR ""; last by auto.
     rewrite /lft_inv_dead. iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)" .
     iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
@@ -197,11 +142,11 @@ Proof.
         as %[EQB1%to_borUR_included _]%auth_valid_discrete_2.
     iDestruct (own_bor_valid_2 with "Hown Hbor2")
         as %[EQB2%to_borUR_included _]%auth_valid_discrete_2.
-    iAssert (⌜j1 ≠ j2⌝)%I with "[#]" as %Hj1j2.
+    iAssert ⌜j1 ≠ j2⌝%I with "[#]" as %Hj1j2.
     { iIntros (->).
       iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
       exfalso. revert Hj1j2. rewrite /= op_singleton singleton_valid.
-      compute. tauto. }
+      by intros [[]]. }
     iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
       as (γ) "(% & Hslice & Hbox)"; first solve_ndisj.
     { done. }
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index 9dd4c7becc3e12c583f2b97f90fb9254270eb423..e5634b26ce71fb7cd0478fe81771f8861648dadb 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -3,22 +3,14 @@ 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 iris.proofmode Require Import tactics.
+(* TODO: move lft_inv_alive_acc, ilft_create and bor_fake to another file. The
+files raw_reborrow, borrow and derived solely depend on this file because of
+the aforementioned lemmas. *)
 
 Section creation.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-(* Lifetime creation *)
-Lemma lft_inh_kill E κ Q :
-  ↑inhN ⊆ E →
-  lft_inh κ false Q ∗ ▷ Q ={E}=∗ lft_inh κ true Q.
-Proof.
-  rewrite /lft_inh. iIntros (?) "[Hinh HQ]".
-  iDestruct "Hinh" as (E') "[Hinh Hbox]".
-  iMod (box_fill with "Hbox HQ") as "?"=>//.
-  rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
-Qed.
-
 Lemma lft_inv_alive_acc (KI K : gset lft) κ :
   (∀ κ', κ' ∈ KI → κ' ⊂ κ → κ' ∈ K) →
   ([∗ set] κ' ∈ K, lft_inv_alive κ') -∗
@@ -33,46 +25,46 @@ Proof.
 Qed.
 
 Lemma ilft_create A I κ :
-  own_ilft_auth I -∗ own_alft_auth A -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
+  own_alft_auth A -∗ own_ilft_auth I -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
       ==∗ ∃ A' I', ⌜is_Some (I' !! κ)⌝ ∗
-    own_ilft_auth I' ∗ own_alft_auth A' ∗ ▷ ([∗ set] κ ∈ dom _ I', lft_inv A' κ).
+    own_alft_auth A' ∗ own_ilft_auth I' ∗ ▷ ([∗ set] κ ∈ dom _ I', lft_inv A' κ).
 Proof.
-  iIntros "HI HA HA'".
+  iIntros "HA HI Hinv".
   destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
   { iModIntro. iExists A, I. by iFrame. }
   iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first done.
   iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
       (frac * dec_agree bor_state)))) as (γbor) "[Hbor Hbor']";
     first by apply auth_valid_discrete_2.
-  iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gset_disj slice_name)))
-    as (γinh) "[Hinh Hinh']"; first by apply auth_valid_discrete_2.
+  iMod (own_alloc ((● ∅) :auth (gset_disj slice_name)))
+     as (γinh) "Hinh"; first by done.
   set (γs := LftNames γbor γcnt γinh).
   iMod (own_update with "HI") as "[HI Hγs]".
   { apply auth_update_alloc,
       (alloc_singleton_local_update _ κ (DecAgree γs)); last done.
     by rewrite lookup_fmap HIκ. }
   iDestruct "Hγs" as "#Hγs".
+  iAssert (own_cnt κ (● 0)) with "[Hcnt]" as "Hcnt".
+  { rewrite /own_cnt. iExists γs. by iFrame. }
+  iAssert (own_cnt κ (◯ 0)) with "[Hcnt']" as "Hcnt'".
+  { rewrite /own_cnt. iExists γs. by iFrame. }
+  iAssert (∀ b, lft_inh κ b True)%I with "[Hinh]" as "Hinh".
+  { iIntros (b). rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
+    iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iFrame. }
   iAssert (lft_inv_dead κ ∧ lft_inv_alive κ)%I
-    with "[-HA HA' HI]" as "Hdeadandalive".
+    with "[-HA HI Hinv]" as "Hdeadandalive".
   { iSplit.
-    - rewrite /lft_inv_dead. iExists True%I. iSplitL "Hbor".
-      { rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !to_gmap_empty.
-        iSplitL "Hbor". iExists γs. by iFrame. iApply box_alloc. }
-      iSplitL "Hcnt".
-      { rewrite /own_cnt. iExists γs. by iFrame. }
-      rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
-      iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iSplit.
+    - rewrite /lft_inv_dead. iExists True%I. iFrame "Hcnt".
+      iSplitL "Hbor"; last by iApply "Hinh".
+      rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !to_gmap_empty.
+      iSplitL "Hbor". iExists γs. by iFrame. iApply box_alloc.
     - rewrite lft_inv_alive_unfold. iExists True%I, True%I. iSplitL "Hbor".
       { rewrite /lft_bor_alive. iExists ∅.
         rewrite /to_borUR !fmap_empty big_sepM_empty.
         iSplitR; [iApply box_alloc|]. iSplit=>//.
         rewrite /own_bor. iExists γs. by iFrame. }
-      rewrite lft_vs_unfold. iSplitR "Hinh".
-      { iExists 0. iSplitL "Hcnt".
-        { rewrite /own_cnt. iExists γs. by iFrame. }
-        iIntros (I') "$ $ _ !>". rewrite /own_cnt. iExists γs. by iFrame. }
-      rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
-      iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iFrame. }
+      iSplitR "Hinh"; last by iApply "Hinh".
+      rewrite lft_vs_unfold. iExists 0. iFrame "Hcnt Hcnt'". auto. }
   destruct (lft_alive_or_dead_in A κ) as [(Λ&?&HAΛ)|Haliveordead].
   - iMod (own_update with "HA") as "[HA _]".
     { apply auth_update_alloc,
@@ -82,24 +74,44 @@ Proof.
     iSplit; first rewrite lookup_insert; eauto.
     rewrite /own_ilft_auth /own_alft_auth /to_ilftUR /to_alftUR !fmap_insert.
     iFrame "HA HI". rewrite dom_insert_L big_sepS_insert ?not_elem_of_dom //.
-    iSplitR "HA'".
+    iSplitR "Hinv".
     { rewrite /lft_inv. iNext. iRight. iSplit.
       { by iDestruct "Hdeadandalive" as "[? _]". }
       iPureIntro. exists Λ. rewrite lookup_insert; auto. }
-    iNext. iApply (@big_sepS_impl with "[$HA']").
+    iNext. iApply (@big_sepS_impl with "[$Hinv]").
     rewrite /lft_inv. iIntros "!#"; iIntros (κ' ?%elem_of_dom)
       "[[HA HA']|[HA HA']]"; iDestruct "HA'" as %HA.
     + iLeft. iFrame "HA". iPureIntro. by apply lft_alive_in_insert.
     + iRight. iFrame "HA". iPureIntro. by apply lft_dead_in_insert.
   - iModIntro. iExists A, (<[κ:=γs]> I).
     iSplit; first rewrite lookup_insert; eauto.
-    iSplitL "HI"; first by rewrite /own_ilft_auth /to_ilftUR fmap_insert.
-    rewrite dom_insert_L big_sepS_insert ?not_elem_of_dom //.
-    iFrame "HA HA'". iNext. rewrite /lft_inv. destruct Haliveordead.
+    rewrite /own_ilft_auth /to_ilftUR fmap_insert. iFrame "HA HI".
+    rewrite dom_insert_L.
+    iApply @big_sepS_insert; first by apply not_elem_of_dom.
+    iFrame "Hinv". iNext. rewrite /lft_inv. destruct Haliveordead.
     + iLeft. by iDestruct "Hdeadandalive" as "[_ $]".
     + iRight. by iDestruct "Hdeadandalive" as "[$ _]".
 Qed.
 
+Lemma bor_fake E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
+Proof.
+  iIntros (?) "#Hmgmt H†". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  iMod (ilft_create _ _ κ with "HA HI Hinv") as (A' I') "(Hκ & HA & HI & Hinv)".
+  iDestruct "Hκ" as %Hκ. rewrite /lft_dead. iDestruct "H†" as (Λ) "[% #H†]".
+  iDestruct (own_alft_auth_agree A' Λ false with "HA H†") as %EQAΛ.
+  iDestruct (@big_sepS_elem_of_acc with "Hinv")
+    as "[Hinv Hclose']"; first by apply elem_of_dom.
+  rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >%]|[Hinv >%]]".
+  { unfold lft_alive_in in *; naive_solver. }
+  rewrite /lft_inv_dead; iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
+  iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
+  unfold bor. iExists κ. iFrame. rewrite -lft_incl_refl.
+  iApply "Hclose". iExists A', I'. iFrame. iNext. iApply "Hclose'".
+  rewrite /lft_inv /lft_inv_dead. iRight. iFrame. eauto.
+Qed.
+
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
   let Iinv := (
     own_ilft_auth I ∗
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 917552ef38724b7237a3003b9518846166e89960..65e6bf460f93d9ae8e49134b633dbd776bd87818 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -1,21 +1,23 @@
-From lrust.lifetime Require Export primitive borrow accessors rebor.
+From lrust.lifetime Require Export primitive accessors creation.
+From lrust.lifetime Require Export raw_reborrow.
 From iris.proofmode Require Import tactics.
+(* TODO: the name derived makes no sense: reborrow/bor_unnest, which is proven
+in the model, depends on this file. *)
 
 Section derived.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-(*** Derived lemmas  *)
-
 Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
 Proof.
   iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic_strong with "LFT Hb") as "[H|[H† Hclose]]"; first done.
-  - iDestruct "H" as (κ') "(Hκκ' & HΦ & Hclose)". iDestruct "HΦ" as (x) "HΦ". iExists x.
-    iApply (bor_shorten with "Hκκ'"). iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
-  - iMod "Hclose" as "_". iExists inhabitant. by iApply (bor_fake with "LFT").
+  iMod (bor_acc_atomic_strong with "LFT Hb") as "[H|[H† >_]]"; first done.
+  - iDestruct "H" as (κ') "(Hκκ' & HΦ & Hclose)".
+    iDestruct "HΦ" as (x) "HΦ". iExists x. iApply (bor_shorten with "Hκκ'").
+    iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
+  - iExists inhabitant. by iApply (bor_fake with "LFT").
 Qed.
 
 Lemma bor_or E κ P Q :
@@ -33,8 +35,9 @@ Proof.
   iIntros (?) "#LFT Hb".
   iMod (bor_acc_atomic_strong with "LFT Hb") as "[H|[H† Hclose]]"; first done.
   - iDestruct "H" as (κ') "(Hκκ' & HP & Hclose)". iModIntro. iNext.
-    iApply (bor_shorten with "Hκκ'"). iApply ("Hclose" with "* HP"). by iIntros "!>$_".
-  - iIntros "!>!>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
+    iApply (bor_shorten with "Hκκ'"). iApply ("Hclose" with "* HP").
+    by iIntros "!> $ _".
+  - iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
 Qed.
 
 Lemma bor_later_tok E q κ P :
@@ -43,7 +46,7 @@ Lemma bor_later_tok E q κ P :
 Proof.
   iIntros (?) "#LFT Hb Htok".
   iMod (bor_acc_strong with "LFT Hb Htok") as (κ') "(Hκκ' & HP & Hclose)"; first done.
-  iModIntro. iNext. iMod ("Hclose" with "* HP []") as "[Hb $]". by iIntros "!>$_".
+  iModIntro. iNext. iMod ("Hclose" with "* HP []") as "[Hb $]". by iIntros "!> $ _".
   by iApply (bor_shorten with "Hκκ'").
 Qed.
 
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 83ccf906a54bc3f19125efd8feed72795d6c932d..5514cece8082e673483474df0681e97a63fd45a7 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -53,6 +53,11 @@ Proof.
   move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
+Global Instance own_bor_into_op κ x x1 x2 :
+  IntoOp x x1 x2 → IntoAnd false (own_bor κ x) (own_bor κ x1) (own_bor κ x2).
+Proof.
+  rewrite /IntoOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_bor_op.
+Qed.
 Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_bor_valid_2 κ x y : own_bor κ x -∗ own_bor κ y -∗ ✓ (x ⋅ y).
@@ -82,6 +87,11 @@ Proof.
   move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
   iExists γs. iSplit; first done. rewrite own_op; iFrame.
 Qed.
+Global Instance own_cnt_into_op κ x x1 x2 :
+  IntoOp x x1 x2 → IntoAnd false (own_cnt κ x) (own_cnt κ x1) (own_cnt κ x2).
+Proof.
+  rewrite /IntoOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_cnt_op.
+Qed.
 Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_cnt_valid_2 κ x y : own_cnt κ x -∗ own_cnt κ y -∗ ✓ (x ⋅ y).
@@ -111,6 +121,11 @@ Proof.
   move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
   iExists γs. iSplit. done. rewrite own_op; iFrame.
 Qed.
+Global Instance own_inh_into_op κ x x1 x2 :
+  IntoOp x x1 x2 → IntoAnd false (own_inh κ x) (own_inh κ x1) (own_inh κ x2).
+Proof.
+  rewrite /IntoOp /IntoAnd=> /leibniz_equiv_iff->. by rewrite -own_inh_op.
+Qed.
 Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_inh_valid_2 κ x y : own_inh κ x -∗ own_inh κ y -∗ ✓ (x ⋅ y).
@@ -274,14 +289,14 @@ Qed.
 
 Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
 Proof.
-  unfold lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
+  rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
   - iIntros (q) "[Hκ'1 Hκ'2]".
     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_sep.
     iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
-    iIntros "!>[Hκ'0 Hκ''0]".
+    iIntros "!> [Hκ'0 Hκ''0]".
     iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
     iApply "Hclose''". iFrame.
   - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
@@ -303,4 +318,92 @@ Proof.
   iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
 Qed.
 
+(** Basic rules about borrows *)
+Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
+Proof.
+  rewrite /bor /raw_bor /idx_bor /bor_idx. iProof; iSplit.
+  - iDestruct 1 as (κ') "[? Hraw]". iDestruct "Hraw" as (s) "[??]".
+    iExists (κ', s). by iFrame.
+  - iDestruct 1 as ([κ' s]) "[[??]?]".
+    iExists κ'. iFrame. iExists s. by iFrame.
+Qed.
+
+Lemma bor_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
+Proof.
+  rewrite /bor. iIntros "#Hκκ'". iDestruct 1 as (i) "[#? ?]".
+  iExists i. iFrame. by iApply (lft_incl_trans with "Hκκ'").
+Qed.
+
+Lemma idx_bor_shorten κ κ' i P : κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
+Proof.
+  rewrite /idx_bor. iIntros "#Hκκ' [#? $]". by iApply (lft_incl_trans with "Hκκ'").
+Qed.
+
+Lemma raw_bor_fake E q κ P :
+  ↑borN ⊆ E →
+  ▷?q lft_bor_dead κ ={E}=∗ ▷?q lft_bor_dead κ ∗ raw_bor κ P.
+Proof.
+  iIntros (?). rewrite /lft_bor_dead. iDestruct 1 as (B Pinh) "[>HB● Hbox]".
+  iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & #Hslice & Hbox)".
+  iMod (own_bor_update with "HB●") as "[HB● H◯]".
+  { eapply auth_update_alloc,
+      (alloc_singleton_local_update _ _ (1%Qp, DecAgree Bor_in)); last done.
+    by do 2 eapply lookup_to_gmap_None. }
+  rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "Hâ—¯".
+  - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
+  - iExists γ. by iFrame.
+Qed.
+
+(* Inheritance *)
+Lemma lft_inh_acc E κ P Q :
+  ↑inhN ⊆ E →
+  ▷ lft_inh κ false Q ={E}=∗ ▷ lft_inh κ false (P ∗ Q) ∗
+     (∀ I, own_ilft_auth I -∗ ⌜is_Some (I !! κ)⌝) ∧
+     (∀ Q', ▷ lft_inh κ true Q' ={E}=∗ ∃ Q'',
+            ▷ ▷ (Q' ≡ (P ∗ Q'')) ∗ ▷ P ∗ ▷ lft_inh κ true Q'').
+Proof.
+  rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
+  iMod (slice_insert_empty _ _ true _ P with "Hbox")
+    as (γE) "(% & #Hslice & Hbox)".
+  iMod (own_inh_update with "HE") as "[HE HEâ—¯]".
+  { by eapply auth_update_alloc, (gset_disj_alloc_empty_local_update _ {[γE]}),
+      disjoint_singleton_l, lookup_to_gmap_None. }
+  iModIntro. iSplitL "Hbox HE".
+  { iNext. rewrite /lft_inh. iExists ({[γE]} ∪ PE).
+    rewrite to_gmap_union_singleton. iFrame. }
+  clear dependent PE. iSplit.
+  { iIntros (I) "HI". iApply (own_inh_auth with "HI HEâ—¯"). }
+  iIntros (Q'). rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
+  iDestruct (own_inh_valid_2 with "HE HEâ—¯")
+    as %[Hle%gset_disj_included _]%auth_valid_discrete_2.
+  iMod (own_inh_update_2 with "HE HEâ—¯") as "HE".
+  { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
+  iMod (slice_delete_full _ _ true with "Hslice Hbox")
+    as (Q'') "($ & #? & Hbox)"; first by solve_ndisj.
+  { rewrite lookup_to_gmap_Some. set_solver. }
+  iModIntro. iExists Q''. iSplit; first done.
+  iNext. rewrite /lft_inh. iExists (PE ∖ {[γE]}). iFrame "HE".
+  rewrite {1}(union_difference_L {[ γE ]} PE); last set_solver.
+  rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None.
+  set_solver.
+Qed.
+
+Lemma lft_inh_kill E κ Q :
+  ↑inhN ⊆ E →
+  lft_inh κ false Q ∗ ▷ Q ={E}=∗ lft_inh κ true Q.
+Proof.
+  rewrite /lft_inh. iIntros (?) "[Hinh HQ]".
+  iDestruct "Hinh" as (E') "[Hinh Hbox]".
+  iMod (box_fill with "Hbox HQ") as "?"=>//.
+  rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
+Qed.
+
+(* View shifts *)
+Lemma lft_vs_frame κ Pb Pi P :
+  lft_vs κ Pb Pi -∗ lft_vs κ (P ∗ Pb) (P ∗ Pi).
+Proof.
+  rewrite !lft_vs_unfold. iDestruct 1 as (n) "[Hcnt Hvs]".
+  iExists n. iFrame "Hcnt". iIntros (I'') "Hinv [$ HPb] H†".
+  iApply ("Hvs" $! I'' with "Hinv HPb H†").
+Qed.
 End primitive.
diff --git a/theories/lifetime/raw_reborrow.v b/theories/lifetime/raw_reborrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..50d7cd713266f0848dc5c6ebc5380b334b1f02ac
--- /dev/null
+++ b/theories/lifetime/raw_reborrow.v
@@ -0,0 +1,164 @@
+From lrust.lifetime Require Export primitive creation.
+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 iris.proofmode Require Import tactics.
+
+Section rebor.
+Context `{invG Σ, lftG Σ}.
+Implicit Types κ : lft.
+
+Lemma raw_bor_unnest E A I Pb Pi P κ κ' :
+  ↑borN ⊆ E →
+  let Iinv := (
+    own_ilft_auth I ∗
+    ▷ [∗ set] κ ∈ dom _ I ∖ {[κ']}, lft_inv A κ)%I in
+  κ ⊆ κ' →
+  lft_alive_in A κ' →
+  Iinv -∗ raw_bor κ P -∗ ▷ lft_bor_alive κ' Pb -∗
+  ▷ lft_vs κ' (raw_bor κ P ∗ Pb) Pi ={E}=∗ ∃ Pb',
+    Iinv ∗ raw_bor κ' P ∗ ▷ lft_bor_alive κ' Pb' ∗ ▷ lft_vs κ' Pb' Pi.
+Proof.
+  iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hinv) Hraw Hκalive' Hvs".
+  destruct (decide (κ = κ')) as [<-|Hκneq].
+  { iModIntro. iExists Pb. rewrite /Iinv. iFrame "HI Hinv Hκalive' Hraw".
+    iNext. rewrite !lft_vs_unfold. iDestruct "Hvs" as (n) "[Hn● Hvs]".
+    iExists n. iFrame "Hn●". clear Iinv I.
+    iIntros (I). rewrite {1}lft_vs_inv_unfold. iIntros "(Hdead & Hinv & Hκs) HPb #Hκ†".
+    iMod (raw_bor_fake _ false _ P with "Hdead") as "[Hdead Hraw]"; first solve_ndisj.
+    iApply ("Hvs" $! I with "[Hdead Hinv Hκs] [HPb Hraw] Hκ†").
+    - rewrite lft_vs_inv_unfold. by iFrame.
+    - by iFrame. }
+  assert (κ ⊂ κ') by (by apply strict_spec_alt).
+  rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hn● Hvs]".
+  iMod (own_cnt_update with "Hn●") as "[Hn● H◯]".
+  { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
+  rewrite {1}/raw_bor /idx_bor_own /=. iDestruct "Hraw" as (i) "[Hi #Hislice]".
+  iDestruct (own_bor_auth with "HI Hi") as %?.
+  iDestruct (@big_sepS_later with "Hinv") as "Hinv".
+  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose]".
+  { by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
+  iDestruct (lft_inv_alive_in with "Hinv") as "Hinv";
+    first by eauto using lft_alive_in_subseteq.
+  rewrite lft_inv_alive_unfold;
+    iDestruct "Hinv" as (Pb' Pi') "(Hκalive&Hvs'&Hinh')".
+  rewrite {2}/lft_bor_alive; iDestruct "Hκalive" as (B) "(Hbox & >HB● & HB)".
+  iDestruct (own_bor_valid_2 with "HB● Hi")
+    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
+  iMod (slice_empty _ _ true with "Hislice Hbox") as "[HP Hbox]"; first done.
+  { by rewrite lookup_fmap HB. }
+  iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
+  { eapply auth_update, singleton_local_update,
+     (exclusive_local_update _ (1%Qp, DecAgree (Bor_rebor κ'))); last done.
+    rewrite /to_borUR lookup_fmap. by rewrite HB. }
+  iDestruct ("Hclose" with "[H◯ HB● HB Hvs' Hinh' Hbox]") as "Hinv".
+  { iNext. rewrite /lft_inv. iLeft.
+    iSplit; last by eauto using lft_alive_in_subseteq.
+    rewrite lft_inv_alive_unfold. iExists Pb', Pi'. iFrame "Hvs' Hinh'".
+    rewrite /lft_bor_alive. iExists (<[i:=Bor_rebor κ']>B).
+    rewrite /to_borUR !fmap_insert. iFrame "Hbox HB●".
+    iDestruct (@big_sepM_delete with "HB") as "[_ HB]"; first done.
+    rewrite (big_sepM_delete _ (<[_:=_]>_) i); last by rewrite lookup_insert.
+    rewrite -insert_delete delete_insert ?lookup_delete //=. iFrame; auto. }
+  clear B HB Pb' Pi'.
+  rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >HB● & HB)".
+  iMod (slice_insert_full _ _ true with "HP Hbox")
+    as (j) "(HBj & #Hjslice & Hbox)"; first done.
+  iDestruct "HBj" as %HBj; move: HBj; rewrite lookup_fmap fmap_None=> HBj.
+  iMod (own_bor_update with "HB●") as "[HB● Hj]".
+  { apply auth_update_alloc,
+     (alloc_singleton_local_update _ j (1%Qp, DecAgree Bor_in)); last done.
+    rewrite /to_borUR lookup_fmap. by rewrite HBj. }
+  iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI". iFrame.
+  iSplitL "Hj".
+  { rewrite /raw_bor /idx_bor_own. iExists j. by iFrame. }
+  iSplitL "Hbox HB● HB".
+  { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
+    rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
+    by rewrite /bor_cnt. }
+  clear dependent Iinv I.
+  iNext. rewrite lft_vs_unfold. iExists (S n). iFrame "Hn●".
+  iIntros (I) "Hinv [HP HPb] #Hκ†".
+  rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
+  iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
+  iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
+  rewrite lft_inv_alive_unfold.
+  iDestruct ("Hκalive" with "[%]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)"; first done.
+  rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
+  iDestruct (own_bor_valid_2 with "HB● Hi") 
+    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
+  iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
+  { eapply auth_update, singleton_local_update,
+     (exclusive_local_update _ (1%Qp, DecAgree Bor_in)); last done.
+    rewrite /to_borUR lookup_fmap. by rewrite HB. }
+  iMod (slice_fill _ _ false with "Hislice HP Hbox")
+     as "Hbox"; first by solve_ndisj.
+  { by rewrite lookup_fmap HB. }
+  iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
+  rewrite /=; iDestruct "Hcnt" as "[% H1â—¯]".
+  iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
+                         [$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
+  { rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
+    iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); first done.
+    iIntros (_). rewrite lft_inv_alive_unfold.
+    iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
+    iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
+    rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
+  { rewrite /raw_bor /idx_bor_own /=. auto. }
+  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
+  by iFrame.
+Qed.
+
+Lemma raw_rebor E κ κ' P :
+  ↑lftN ⊆ E → κ ⊆ κ' →
+  lft_ctx -∗ raw_bor κ P ={E}=∗
+    raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
+Proof.
+  rewrite /lft_ctx. iIntros (??) "#LFT Hκ".
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  iMod (ilft_create _ _ κ' with "HA HI Hinv") as (A' I') "(% & HA & HI & Hinv)".
+  clear A I; rename A' into A; rename I' into I.
+  iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
+    first by apply elem_of_dom.
+  rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[? >%]|[Hdead >%]]"; last first.
+  { rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & >H● & Hinh)".
+    iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead $]"; first solve_ndisj.
+    iMod ("Hclose" with "[-Hκ]") as "_"; last auto.
+    iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
+    iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom.
+    iFrame "Hinv". rewrite /lft_inv /lft_inv_dead. iRight. iSplit; last done.
+    iExists Pi. by iFrame. }
+  rewrite lft_inv_alive_unfold; iDestruct "Hκinv'" as (Pb Pi) "(Hbor & Hvs & Hinh)".
+  iMod (lft_inh_acc _ _ (raw_bor κ P) with "Hinh")
+    as "[Hinh Hinh_close]"; first solve_ndisj.
+  iMod (raw_bor_unnest _ _ _ _ (raw_bor κ P ∗ Pi)%I with "[$HI $Hinv] Hκ Hbor [Hvs]")
+    as (Pb') "([HI Hinv] & $ & Halive & Hvs)"; [solve_ndisj|done|done|..].
+  { iNext. by iApply lft_vs_frame. }
+  iMod ("Hclose" with "[HA HI Hinv Halive Hinh Hvs]") as "_".
+  { iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
+    iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
+    rewrite /lft_inv. iLeft. iSplit; last done.
+    rewrite lft_inv_alive_unfold. iExists Pb', (raw_bor κ P ∗ Pi)%I. iFrame. }
+  iModIntro. iIntros "H†".
+  clear dependent A I Pb Pb' Pi.
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  iAssert ⌜ is_Some (I !! κ') ⌝%I with "[#]" as %Hκ'.
+  { iDestruct "Hinh_close" as "[H _]". by iApply "H". }
+  iDestruct "Hinh_close" as "[_ Hinh_close]".
+  iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
+    first by apply elem_of_dom.
+  rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[Halive >%]|[Hdead >%]]".
+  - (* the same proof is in bor_fake and bor_create *)
+    rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
+    iDestruct (own_alft_auth_agree A Λ false with "HA H†") as %EQAΛ.
+    unfold lft_alive_in in *. naive_solver.
+  - rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & Hcnt & Hinh)".
+    iMod ("Hinh_close" $! Pi with "Hinh") as (Pi') "(Heq & Hbor & Hinh)".
+    iMod ("Hclose" with "[HA HI Hinv Hdead Hinh Hcnt]") as "_".
+    { iNext. rewrite /lfts_inv. iExists A, I. iFrame "HA HI".
+      iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
+      rewrite /lft_inv /lft_inv_dead. iRight. iSplit; last done.
+      iExists Pi'. iFrame. }
+    iModIntro. rewrite /raw_bor. (* oops, later trouble... *)
+Admitted.
+End rebor.
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
deleted file mode 100644
index bba7edeeb34ad2a867db6b5913015c6c76ad7dc6..0000000000000000000000000000000000000000
--- a/theories/lifetime/rebor.v
+++ /dev/null
@@ -1,160 +0,0 @@
-From lrust.lifetime Require Export primitive.
-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 iris.proofmode Require Import tactics.
-
-Section rebor.
-Context `{invG Σ, lftG Σ}.
-Implicit Types κ : lft.
-
-Lemma raw_bor_fake E q κ P :
-  ↑borN ⊆ E →
-  ▷?q lft_bor_dead κ ={E}=∗ ▷?q lft_bor_dead κ ∗ raw_bor κ P.
-Proof.
-  iIntros (?) "Hdead". rewrite /lft_bor_dead.
-  iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
-  iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & #Hslice & Hbox)".
-  iMod (own_bor_update with "Hown") as "Hown".
-  { eapply auth_update_alloc,
-      (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
-    by do 2 eapply lookup_to_gmap_None. }
-  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own /=. 
-  iModIntro. iDestruct "Hown" as "[H● H◯]". iSplitR "H◯".
-  - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
-  - iExists γ. by iFrame.
-Qed.
-
-Lemma raw_bor_unnest A I Pb Pi P κ κ' :
-  let Iinv := (
-    own_ilft_auth I ∗
-    ▷ [∗ set] κ ∈ dom _ I ∖ {[κ']}, lft_inv A κ)%I in
-  κ ⊆ κ' →
-  lft_alive_in A κ' →
-  Iinv -∗ raw_bor κ P -∗ ▷ lft_bor_alive κ' Pb -∗
-  ▷ lft_vs κ' (Pb ∗ raw_bor κ P) Pi ={↑borN}=∗ ∃ Pb',
-    Iinv ∗ raw_bor κ' P ∗ ▷ lft_bor_alive κ' Pb' ∗ ▷ lft_vs κ' Pb' Pi.
-Proof.
-  iIntros (Iinv Hκκ' Haliveκ') "(HI● & HI) Hraw Hκalive' Hvs".
-  destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iModIntro. iExists Pb. rewrite /Iinv. iFrame "HI● HI Hκalive' Hraw".
-    iNext. rewrite !lft_vs_unfold. iDestruct "Hvs" as (n) "[Hn Hvs]".
-    iExists n. iFrame "Hn". clear Iinv I.
-    iIntros (I). rewrite {1}lft_vs_inv_unfold. iIntros "(Hdead & HI & Hκs) HPb #Hκ†".
-    iMod (raw_bor_fake _ false _ P with "Hdead") as "[Hdead Hraw]"; first solve_ndisj.
-    iApply ("Hvs" $! I with "[Hdead HI Hκs] [HPb Hraw] Hκ†").
-    - rewrite lft_vs_inv_unfold. by iFrame.
-    - iNext. by iFrame. }
-  assert (κ ⊂ κ') by (by apply strict_spec_alt).
-  rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hcnt Hvs]".
-  iMod (own_cnt_update with "Hcnt") as "Hcnt".
-  { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
-  rewrite own_cnt_op; iDestruct "Hcnt" as "[Hcnt Hcnt1]".
-  rewrite {1}/raw_bor /idx_bor_own /=. iDestruct "Hraw" as (i) "[Hbor #Hislice]".
-  iDestruct (own_bor_auth with "HI● Hbor") as %?.
-  rewrite big_sepS_later.
-  iDestruct (big_sepS_elem_of_acc _ (dom (gset lft) I ∖ _) κ with "HI")
-    as "[HAκ HI]".
-  { by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
-  iDestruct (lft_inv_alive_in with "HAκ") as "Hκalive";
-    first by eauto using lft_alive_in_subseteq.
-  rewrite lft_inv_alive_unfold;
-    iDestruct "Hκalive" as (Pb' Pi') "(Hbor'&Hvs'&Hinh')".
-  rewrite {2}/lft_bor_alive; iDestruct "Hbor'" as (B) "(Hbox & >HκB & HB)".
-  iDestruct (own_bor_valid_2 with "HκB Hbor")
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (slice_empty _ _ true with "Hislice Hbox") as "[HP Hbox]"; first done.
-  { by rewrite lookup_fmap HB. }
-  iMod (own_bor_update_2 with "HκB Hbor") as "HFOO".
-  { eapply auth_update, singleton_local_update,
-     (exclusive_local_update _ (1%Qp, DecAgree (Bor_rebor κ'))); last done.
-    rewrite /to_borUR lookup_fmap. by rewrite HB. }
-  rewrite own_bor_op. iDestruct "HFOO" as "[HκB Hrebor]".
-  iSpecialize ("HI" with "[Hcnt1 HB Hvs' Hinh' Hbox HκB]").
-  { iNext. rewrite /lft_inv. iLeft.
-    iSplit; last by eauto using lft_alive_in_subseteq.
-    rewrite lft_inv_alive_unfold. iExists Pb', Pi'. iFrame "Hvs' Hinh'".
-    rewrite /lft_bor_alive. iExists (<[i:=Bor_rebor κ']>B).
-    rewrite /to_borUR !fmap_insert. iFrame "Hbox HκB".
-    iDestruct (@big_sepM_delete with "HB") as "[_ HB]"; first done.
-    rewrite (big_sepM_delete _ (<[_:=_]>_) i); last by rewrite lookup_insert.
-    rewrite -insert_delete delete_insert ?lookup_delete //.
-    iFrame; simpl; auto. }
-  clear B HB Pb' Pi'.
-  rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >Hbor & HB)".
-  iMod (slice_insert_full _ _ true with "HP Hbox")
-    as (j) "(HBj & #Hjslice & Hbox)"; first done.
-  iDestruct "HBj" as %HBj. move: HBj; rewrite lookup_fmap fmap_None=> HBj.
-  iMod (own_bor_update with "Hbor") as "HFOO".
-  { apply auth_update_alloc,
-     (alloc_singleton_local_update _ j (1%Qp, DecAgree Bor_in)); last done.
-    rewrite /to_borUR lookup_fmap. by rewrite HBj. }
-  rewrite own_bor_op. iDestruct "HFOO" as "[HκB Hj]".
-  iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI● HI".
-  iSplitL "Hj".
-  { rewrite /raw_bor /idx_bor_own. iExists j. by iFrame. }
-  iSplitL "HB HκB Hbox".
-  { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
-    rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
-    by rewrite /bor_cnt. }
-  clear dependent Iinv I.
-  iNext. rewrite lft_vs_unfold. iExists (S n). iFrame "Hcnt".
-  iIntros (I) "Hinv [HP HPb] Hκ'".
-  rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hdead&HI&Hκs)".
-  iDestruct (own_bor_auth with "HI Hrebor") as %?%elem_of_dom.
-  iDestruct (@big_sepS_delete with "Hκs") as "[Hκ Hκs]"; first done.
-  rewrite lft_inv_alive_unfold.
-  iDestruct ("Hκ" with "[%]") as (Pb' Pi') "(Halive&Hvs'&Hinh)"; first done.
-  rewrite /lft_bor_alive; iDestruct "Halive" as (B') "(Hbox & Hbor & HB)".
-  iDestruct (own_bor_valid_2 with "Hbor Hrebor") 
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (own_bor_update_2 with "Hbor Hrebor") as "HFOO".
-  { eapply auth_update, singleton_local_update,
-     (exclusive_local_update _ (1%Qp, DecAgree Bor_in)); last done.
-    rewrite /to_borUR lookup_fmap. by rewrite HB. }
-  rewrite own_bor_op. iDestruct "HFOO" as "[Hbor Hrebor]".
-  iMod (slice_fill _ _ false with "Hislice HP Hbox") as "Hbox"; first by solve_ndisj.
-  { by rewrite lookup_fmap HB. }
-  iDestruct (@big_sepM_delete with "HB") as "[Hκ HB]"; first done.
-  rewrite /=; iDestruct "Hκ" as "[% Hcnt]".
-  iMod ("Hvs" $! I with "[Hdead HI Hκs Hbox Hvs' Hinh Hbor HB]
-                         [$HPb Hrebor] Hκ'") as "($&$&Hcnt')".
-  { rewrite lft_vs_inv_unfold. iFrame "Hdead HI".
-    iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hκs]"); first done.
-    iIntros (_). rewrite lft_inv_alive_unfold.
-    iExists Pb', Pi'. iFrame "Hvs' Hinh". rewrite /lft_bor_alive.
-    iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
-    rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
-  { rewrite /raw_bor /idx_bor_own /=. iFrame; auto. }
-  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
-  by iFrame.
-Qed.
-
-Lemma raw_rebor E κ κ' P :
-  ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx -∗ raw_bor κ P ={E}=∗
-    raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
-Admitted.
-
-Lemma bor_rebor' E κ κ' P :
-  ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx -∗ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
-Proof. Admitted.
-Lemma rebor E P κ κ' :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
-Proof.
-  iIntros (?) "#LFT #H⊑ HP". (* iMod (bor_rebor' with "LFT HP") as "[Hκ' H∋]".
-    done. by exists κ'.
-  iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
-  { iApply lft_incl_lb. iSplit. done. iApply lft_incl_refl. }
-  iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
-Qed.
-*)
-Admitted.
-
-Lemma bor_unnest E κ κ' P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
-Proof. Admitted.
-End rebor.
diff --git a/theories/lifetime/reborrow.v b/theories/lifetime/reborrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..8321443f091b9966eeaf972f9ba2b31e22de859f
--- /dev/null
+++ b/theories/lifetime/reborrow.v
@@ -0,0 +1,40 @@
+From lrust.lifetime Require Export derived.
+From lrust.lifetime Require Export raw_reborrow.
+From iris.base_logic Require Import big_op.
+From iris.base_logic.lib Require Import boxes.
+From iris.proofmode Require Import tactics.
+
+Section reborrow.
+Context `{invG Σ, lftG Σ}.
+Implicit Types κ : lft.
+
+Lemma rebor E κ κ' P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
+Proof.
+  iIntros (?) "#LFT #H⊑". rewrite {1}/bor; iDestruct 1 as (κ'') "[#H⊑' Hκ'']".
+  iMod (raw_rebor _ _ (κ' ∪ κ'') with "LFT Hκ''") as "[Hκ'' Hclose]"; first done.
+  { apply gmultiset_union_subseteq_r. }
+  iModIntro. iSplitL "Hκ''".
+  - rewrite /bor. iExists (κ' ∪ κ''). iFrame "Hκ''".
+    iApply (lft_incl_glb with "[]"); first iApply lft_incl_refl.
+    by iApply (lft_incl_trans with "H⊑").
+  - iIntros "Hκ†". iMod ("Hclose" with "[Hκ†]") as "Hκ''".
+    { iApply lft_dead_or; auto. }
+    iModIntro. rewrite /bor. eauto. 
+Qed.
+
+Lemma bor_unnest E κ κ' P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
+Proof.
+  iIntros (?) "#LFT Hκ'". rewrite {2}/bor.
+  iMod (bor_exists with "LFT Hκ'") as (κ'') "Hκ'"; first done.
+  rewrite {1}/bor; iDestruct "Hκ'" as (κ''') "[#H⊑' Hκ''']".
+(*
+  iMod (raw_rebor _ _ (κ'' ∪ κ''') with "LFT Hκ'''") as "[Hκ Hclose]"; first done.
+  { apply gmultiset_union_subseteq_r. }
+Check   
+Qed. *)
+Admitted.
+End reborrow.
\ No newline at end of file
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 4f5042ef4c7e63c05d7cb32aea0fd79835dd8461..5584c2d53ac6fcbb3afd1f9e310b671bb127abaa 100644
--- a/theories/lifetime/shr_borrow.v
+++ b/theories/lifetime/shr_borrow.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import gmap auth frac.
 From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Export derived.
+From lrust.lifetime Require Export borrow derived.
 
 (** Shared bors  *)
 Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
diff --git a/theories/typing/perm_incl.v b/theories/typing/perm_incl.v
index 8791ec050e943875fbfa01102529372ddd6f6d37..162bfe6dc6c533e4e32323751f8257acdeec96cf 100644
--- a/theories/typing/perm_incl.v
+++ b/theories/typing/perm_incl.v
@@ -1,7 +1,7 @@
 From Coq Require Import Qcanon.
 From iris.base_logic Require Import big_op.
 From lrust.typing Require Export type perm.
-From lrust.lifetime Require Import frac_borrow.
+From lrust.lifetime Require Import frac_borrow reborrow.
 
 Import Perm Types.
 
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 8f3bdd31ca2fa2e440b8322bb3162b197789f1aa..9b64209deea0d4537071d52cd8ebc4e8657d967b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Export thread_local.
 From iris.program_logic Require Import hoare.
 From lrust.lang Require Export heap notation.
-From lrust.lifetime Require Import frac_borrow.
+From lrust.lifetime Require Import frac_borrow reborrow.
 
 Class iris_typeG Σ := Iris_typeG {
   type_heapG :> heapG Σ;
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index ae5d0051f60a3c0586059a2755f8524f96639626..0fc72fa3cb56f922b9dcf814f3d7f2175cc3989b 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -3,7 +3,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Export notation memcpy.
 From lrust.typing Require Export type perm.
 From lrust Require Import typing.perm_incl lang.proofmode.
-From lrust.lifetime Require Import frac_borrow.
+From lrust.lifetime Require Import frac_borrow reborrow.
 
 Import Types Perm.