diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index e5cbde2ad42defea9c5918c0724793871cecbb84..b2b787971b3f64413adbd69107cca91e07db3a44 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -26,6 +26,21 @@ Section derived.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
+Lemma bor_acc_atomic_cons E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
+    (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+    ([†κ] ∗ |={E∖↑lftN,E}=> True).
+Proof.
+  iIntros (?) "#LFT HP".
+  iMod (bor_acc_atomic_strong with "LFT HP") as "[H|[??]]"; first done.
+  - iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>* HPQ HQ".
+    iMod ("Hclose" with "[HPQ] HQ") as "Hb".
+    + iNext. iIntros "? _". by iApply "HPQ".
+    + iApply (bor_shorten with "Hκκ' Hb").
+  - iRight. by iFrame.
+Qed.
+
 Lemma bor_acc_atomic E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index f2dd298f45b928fbb2a14cbc6214cadbb7cc77ac..0492383bd3dc9d335617be509deefb7d71c5abeb 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -62,12 +62,12 @@ Module Type lifetime_sig.
   Global Declare Instance lft_intersect_right_id : RightId eq static lft_intersect.
 
   Global Declare Instance lft_ctx_persistent : PersistentP lft_ctx.
-  Global Declare Instance lft_dead_persistent κ : PersistentP (lft_dead κ).
+  Global Declare Instance lft_dead_persistent κ : PersistentP ([†κ]).
   Global Declare Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
-  Global Declare Instance idx_bor_persistent κ i P : PersistentP (idx_bor κ i P).
+  Global Declare Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
 
-  Global Declare Instance lft_tok_timeless q κ : TimelessP (lft_tok q κ).
-  Global Declare Instance lft_dead_timeless κ : TimelessP (lft_dead κ).
+  Global Declare Instance lft_tok_timeless q κ : TimelessP (q.[κ]).
+  Global Declare Instance lft_dead_timeless κ : TimelessP ([†κ]).
   Global Declare Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
 
   Global Instance idx_bor_params : Params (@idx_bor) 5.
@@ -151,11 +151,6 @@ Module Type lifetime_sig.
     □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
                  lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
         (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
-  (* Same for some of the derived lemmas. *)
-  Parameter bor_acc_atomic_cons : ∀ E κ P,
-    ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-      (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
-      ([†κ] ∗ |={E∖↑lftN,E}=> True).
 
   End properties.
 
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 053a65ce864f967aae570d6f37d2b7c67da88832..1dbe120693d240af40513016a8e528b6c35122a1 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -262,20 +262,4 @@ Proof.
     + iMod (lft_incl_dead with "Hle H†") as "$". done.
       iApply fupd_intro_mask'. solve_ndisj.
 Qed.
-
-(* These derived lemmas are needed inside the model. *)
-Lemma bor_acc_atomic_cons E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-    (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
-    ([†κ] ∗ |={E∖↑lftN,E}=> True).
-Proof.
-  iIntros (?) "#LFT HP".
-  iMod (bor_acc_atomic_strong with "LFT HP") as "[H|[??]]"; first done.
-  - iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>* HPQ HQ".
-    iMod ("Hclose" with "[HPQ] HQ") as "Hb".
-    + iNext. iIntros "? _". by iApply "HPQ".
-    + iApply (bor_shorten with "Hκκ' Hb").
-  - iRight. by iFrame.
-Qed.
 End accessors.