diff --git a/_CoqProject b/_CoqProject
index 67a059fc33d5617a4f17abc3f33848c4088ae681..99d284ab9a620e7face66e98e0d56c74f7b4b112 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,7 +4,7 @@ theories/lifetime/definitions.v
 theories/lifetime/derived.v
 theories/lifetime/creation.v
 theories/lifetime/primitive.v
-theories/lifetime/todo.v
+theories/lifetime/accessors.v
 theories/lifetime/borrow.v
 theories/lifetime/rebor.v
 theories/lifetime/shr_borrow.v
diff --git a/theories/lifetime/todo.v b/theories/lifetime/accessors.v
similarity index 97%
rename from theories/lifetime/todo.v
rename to theories/lifetime/accessors.v
index b04360b6ee797a87018d9999b3153b5cd8057ca0..3c74848b7921d164cd994ccc18112a09ca7ad400 100644
--- a/theories/lifetime/todo.v
+++ b/theories/lifetime/accessors.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export definitions.
 
-Section todo.
+Section accessors.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
@@ -31,4 +31,4 @@ Lemma idx_bor_atomic_acc E q κ i P :
               [†κ] ∗ (|={E∖↑lftN,E}=> idx_bor_own q i).
 Proof. Admitted.
 
-End todo.
\ No newline at end of file
+End accessors.
\ No newline at end of file
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index 2cfa33a7f7c66d9d2875ad4f8911cb58497def0f..239a0e222f8a0aa2d8148db7bbd977cec0bc8efb 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive creation.
+From lrust.lifetime Require Export primitive creation rebor.
 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.
@@ -23,22 +23,6 @@ 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 raw_bor_fake E κ P :
-  ↑borN ⊆ E →
-  ▷ lft_bor_dead κ ={E}=∗ ∃ i, ▷ lft_bor_dead κ ∗ raw_bor (κ, i) P.
-Proof.
-  iIntros (?) "Hdead". rewrite /lft_bor_dead.
-  iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
-  iMod (box_insert_empty _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
-  iMod (own_bor_update with "Hown") as "Hown".
-  { apply auth_update_alloc.
-    apply: (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
-    do 2 eapply lookup_to_gmap_None. by eauto. }
-  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own. iExists _.
-  iDestruct "Hown" as "[H● H◯]". iSplitL "H● Hbox"; last by eauto.
-  iExists _, _. rewrite -!to_gmap_union_singleton. by iFrame.
-Qed.
-
 Lemma bor_fake E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
@@ -177,12 +161,6 @@ Proof.
     unfold bor. iSplitL "Hbor1"; iExists (_, _); eauto.
 Qed.
 
-Lemma raw_rebor E κ κ' i P :
-  ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx -∗ raw_bor (κ, i) P ={E}=∗
-    ∃ j, raw_bor (κ', j) P ∗ ([†κ'] ={E}=∗ raw_bor (κ, i) P).
-Admitted.
-
 Lemma bor_combine E κ P Q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index e326230051083dfa27cefe1903caa2e0e3a68ef7..263a0af2d56d69a4f14e71e580b22201d4d61221 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive borrow todo.
+From lrust.lifetime Require Export primitive borrow accessors rebor.
 From iris.proofmode Require Import tactics.
 
 Section derived.
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index 7fe8f7e7d4e222798b78e56e3ba14d66ffa67e12..410d07a6bf681bdda42f46614a972bfcb801d701 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive (* borrow *).
+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.
@@ -12,6 +12,22 @@ Section rebor.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
+Lemma raw_bor_fake E κ P :
+  ↑borN ⊆ E →
+  ▷ lft_bor_dead κ ={E}=∗ ∃ i, ▷ lft_bor_dead κ ∗ raw_bor (κ, i) P.
+Proof.
+  iIntros (?) "Hdead". rewrite /lft_bor_dead.
+  iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
+  iMod (box_insert_empty _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
+  iMod (own_bor_update with "Hown") as "Hown".
+  { apply auth_update_alloc.
+    apply: (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
+    do 2 eapply lookup_to_gmap_None. by eauto. }
+  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own. iExists _.
+  iDestruct "Hown" as "[H● H◯]". iSplitL "H● Hbox"; last by eauto.
+  iExists _, _. rewrite -!to_gmap_union_singleton. by iFrame.
+Qed.
+
 Lemma raw_bor_unnest A I Pb Pi P κ κ' i :
   let Iinv := (
     own_ilft_auth I ∗
@@ -115,6 +131,13 @@ admit.
 
 Admitted.
 
+
+Lemma raw_rebor E κ κ' i P :
+  ↑lftN ⊆ E → κ ⊆ κ' →
+  lft_ctx -∗ raw_bor (κ, i) P ={E}=∗
+    ∃ j, raw_bor (κ', j) P ∗ ([†κ'] ={E}=∗ raw_bor (κ, i) P).
+Admitted.
+
 Lemma bor_rebor' E κ κ' P :
   ↑lftN ⊆ E → κ ⊆ κ' →
   lft_ctx -∗ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
@@ -131,8 +154,10 @@ Proof.
 Qed.
 *)
 Admitted.
+
 Lemma bor_unnest E κ κ' P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
 Proof. Admitted.
+
 End rebor.
diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index 4f0b536a07d6f6e1d5d2abdab2c0796a124c65c8..7e88e51a27fd4afcc50f1b6ff08bf6cbfb6e83e9 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From lrust.typing Require Export type.
 From lrust.lang Require Export proofmode.
-From lrust.lifetime Require Import derived.
+From lrust.lifetime Require Import frac_borrow.
 
 Delimit Scope perm_scope with P.
 Bind Scope perm_scope with perm.
diff --git a/theories/typing/perm_incl.v b/theories/typing/perm_incl.v
index 15ed02de4124b1caf263e25d890bfba456afea2b..8791ec050e943875fbfa01102529372ddd6f6d37 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 rebor.
+From lrust.lifetime Require Import frac_borrow.
 
 Import Perm Types.
 
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 07430ccb7d2673aaf885f1d94c9f8c752c52f90f..2f7e5ea823c90f662aa99389cc3241c7f159185b 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 rebor.
+From lrust.lifetime Require Import frac_borrow.
 
 Class iris_typeG Σ := Iris_typeG {
   type_heapG :> heapG Σ;
diff --git a/theories/typing/type_incl.v b/theories/typing/type_incl.v
index efe320a0a905433b1a97fb0faf20a68d5c496c88..060c52bcf09c573e1b50de35b55813966f0afa5d 100644
--- a/theories/typing/type_incl.v
+++ b/theories/typing/type_incl.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Import big_op.
 From iris.program_logic Require Import hoare.
 From lrust.typing Require Export type perm_incl.
-From lrust.lifetime Require Import derived frac_borrow.
+From lrust.lifetime Require Import frac_borrow.
 
 Import Types.
 
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 28e6e81c2063b27cfc0fdaee35704e62b31511b3..f9d4063712724f535ec6bfff248fbfbcfb1c208e 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 rebor.
+From lrust.lifetime Require Import frac_borrow.
 
 Import Types Perm.