diff --git a/_CoqProject b/_CoqProject
index 13d7b219355d675b4293f0e0530a1950503c8f88..f4938067aa076015e602adf7bfd9ec0638652b36 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,13 +1,14 @@
 -Q theories lrust
-theories/lifetime/definitions.v
-theories/lifetime/derived.v
-theories/lifetime/faking.v
-theories/lifetime/creation.v
-theories/lifetime/primitive.v
-theories/lifetime/accessors.v
-theories/lifetime/raw_reborrow.v
-theories/lifetime/borrow.v
-theories/lifetime/reborrow.v
+theories/lifetime/model/definitions.v
+theories/lifetime/model/faking.v
+theories/lifetime/model/creation.v
+theories/lifetime/model/primitive.v
+theories/lifetime/model/accessors.v
+theories/lifetime/model/raw_reborrow.v
+theories/lifetime/model/borrow.v
+theories/lifetime/model/reborrow.v
+theories/lifetime/lifetime_sig.v
+theories/lifetime/lifetime.v
 theories/lifetime/shr_borrow.v
 theories/lifetime/frac_borrow.v
 theories/lifetime/na_borrow.v
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 77084d69e77214874822756a6f371205600521cb..e491ea982df64923c1c8e61aee6feda84d808d72 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -2,7 +2,7 @@ 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.lifetime Require Export shr_borrow .
+From lrust.lifetime Require Export shr_borrow.
 Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
@@ -128,7 +128,7 @@ Section frac_bor.
   Lemma frac_bor_lft_incl κ κ' q:
     lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
   Proof.
-    iIntros "#LFT#Hbor!#". iSplitR.
+    iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iSplitR.
     - iIntros (q') "Hκ'".
       iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
       iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
diff --git a/theories/lifetime/derived.v b/theories/lifetime/lifetime.v
similarity index 66%
rename from theories/lifetime/derived.v
rename to theories/lifetime/lifetime.v
index ecf3524f857dde16b22020a7daa9aa45160f9a74..9ee11aa4c200efc1d625349a64ed0421bec0ec8e 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/lifetime.v
@@ -1,23 +1,42 @@
-From lrust.lifetime Require Export primitive accessors faking.
-From lrust.lifetime Require Export raw_reborrow.
+From lrust.lifetime Require Export lifetime_sig.
+From lrust.lifetime.model Require definitions primitive accessors faking borrow
+     reborrow creation.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
-(* TODO: the name derived makes no sense: reborrow/bor_unnest, which is proven
-in the model, depends on this file. *)
+
+Module Export lifetime : lifetime_sig.
+  Include definitions.
+  Include primitive.
+  Include borrow.
+  Include faking.
+  Include reborrow.
+  Include accessors.
+  Include creation.
+End lifetime.
 
 Section derived.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
+Lemma bor_acc_cons E q κ P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+  lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
+    ∀ Q, ▷ Q -∗ ▷(▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
 Proof.
-  iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
-  - iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
-    iExists x. iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
-  - iExists inhabitant. by iApply (bor_fake with "LFT").
+  iIntros (?) "#LFT HP Htok".
+  iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
+  iIntros "!>*HQ HPQ". iMod ("Hclose" with "*HQ [HPQ]") as "[Hb $]".
+  - iNext. iIntros "? _". by iApply "HPQ".
+  - iApply (bor_shorten with "Hκκ' Hb").
+Qed.
+
+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_cons with "LFT HP Htok") as "($ & Hclose)"; first done.
+  iIntros "!>HP". iMod ("Hclose" with "*HP []") as "[$ $]"; auto.
 Qed.
 
 Lemma bor_or E κ P Q :
@@ -80,8 +99,9 @@ Qed.
 
 Lemma lft_incl_static κ : (κ ⊑ static)%I.
 Proof.
-  iIntros "!#". iSplitR.
+  iApply lft_incl_intro. iIntros "!#". iSplitR.
   - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
   - iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
 Qed.
 End derived.
+
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
new file mode 100644
index 0000000000000000000000000000000000000000..ea1cb375a425ad8ed01d22e3d815ebf50ef78547
--- /dev/null
+++ b/theories/lifetime/lifetime_sig.v
@@ -0,0 +1,180 @@
+From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.prelude Require Export gmultiset strings.
+From iris.base_logic.lib Require Export invariants.
+From iris.base_logic.lib Require Import boxes fractional.
+Set Default Proof Using "Type".
+
+Definition lftN : namespace := nroot .@ "lft".
+Definition borN : namespace := lftN .@ "bor".
+Definition inhN : namespace := lftN .@ "inh".
+Definition mgmtN : namespace := lftN .@ "mgmt".
+
+Definition atomic_lft := positive.
+Notation lft := (gmultiset positive).
+Definition static : lft := ∅.
+
+Inductive bor_state :=
+  | Bor_in
+  | Bor_open (q : frac)
+  | Bor_rebor (κ : lft).
+Instance bor_state_eq_dec : EqDecision bor_state.
+Proof. solve_decision. Defined.
+Canonical bor_stateC := leibnizC bor_state.
+
+Record lft_names := LftNames {
+  bor_name : gname;
+  cnt_name : gname;
+  inh_name : gname
+}.
+Instance lft_names_eq_dec : EqDecision lft_names.
+Proof. solve_decision. Defined.
+Canonical lft_namesC := leibnizC lft_names.
+
+Definition lft_stateR := csumR fracR unitR.
+Definition alftUR := gmapUR atomic_lft lft_stateR.
+Definition ilftUR := gmapUR lft (agreeR lft_namesC).
+Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
+Definition inhUR := gset_disjUR slice_name.
+
+Class lftG Σ := LftG {
+  lft_box :> boxG Σ;
+  alft_inG :> inG Σ (authR alftUR);
+  alft_name : gname;
+  ilft_inG :> inG Σ (authR ilftUR);
+  ilft_name : gname;
+  lft_bor_inG :> inG Σ (authR borUR);
+  lft_cnt_inG :> inG Σ (authR natUR);
+  lft_inh_inG :> inG Σ (authR inhUR);
+}.
+
+Module Type lifetime_sig.
+  (** Definitions *)
+  Parameter lft_ctx : ∀ `{invG, lftG Σ}, iProp Σ.
+
+  Parameter lft_tok : ∀ `{lftG Σ} (q : Qp) (κ : lft), iProp Σ.
+  Parameter lft_dead : ∀ `{lftG Σ} (κ : lft), iProp Σ.
+
+  Parameter lft_incl : ∀ `{invG, lftG Σ} (κ κ' : lft), iProp Σ.
+  Parameter bor : ∀ `{invG, lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
+
+  Parameter bor_idx : Type.
+  Parameter idx_bor_own : ∀ `{lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
+  Parameter idx_bor : ∀ `{invG, lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+  
+  Notation "q .[ κ ]" := (lft_tok q κ)
+      (format "q .[ κ ]", at level 0) : uPred_scope.
+  Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
+
+  Notation "&{ κ } P" := (bor κ P)
+    (format "&{ κ }  P", at level 20, right associativity) : uPred_scope.
+  Notation "&{ κ , i } P" := (idx_bor κ i P)
+    (format "&{ κ , i }  P", at level 20, right associativity) : uPred_scope.
+
+  Infix "⊑" := lft_incl (at level 70) : uPred_scope.
+
+  Section properties.
+  Context `{invG, lftG Σ}.
+
+  (** Instances *)
+  Global Declare Instance lft_ctx_persistent : PersistentP lft_ctx.
+  Global Declare Instance lft_dead_persistent κ : PersistentP (lft_dead κ).
+  Global Declare Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
+  Global Declare Instance idx_bor_persistent κ i P : PersistentP (idx_bor κ 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 idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
+
+  Global Instance idx_bor_params : Params (@idx_bor) 5.
+  Global Instance bor_params : Params (@bor) 4.
+
+  Global Declare Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
+  Global Declare Instance bor_contractive κ : Contractive (bor κ).
+  Global Declare Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
+  Global Declare Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
+  Global Declare Instance idx_bor_contractive κ i : Contractive (idx_bor κ i).
+  Global Declare Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
+
+  Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
+  Global Declare Instance lft_tok_as_fractional κ q :
+    AsFractional q.[κ] (λ q, q.[κ])%I q.
+  Global Declare Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
+  Global Declare Instance idx_bor_own_as_fractional i q :
+    AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
+
+  (** Laws *)
+  Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
+  Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [† κ1 ∪ κ2].
+  Parameter lft_tok_dead : ∀ q κ, q.[κ] -∗ [† κ] -∗ False.
+  Parameter lft_tok_static : ∀ q, q.[static]%I.
+  Parameter lft_dead_static : [† static] -∗ False.
+
+  Parameter lft_create : ∀ E, ↑lftN ⊆ E →
+    lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
+  Parameter bor_create : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
+  Parameter bor_fake : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
+
+  Parameter bor_sep : ∀ E κ P Q,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
+  Parameter bor_combine : ∀ E κ P Q,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
+
+  Parameter bor_unfold_idx : ∀ κ P, &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
+  Parameter bor_shorten : ∀ κ κ' P, κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
+  Parameter idx_bor_shorten : ∀ κ κ' i P, κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
+
+  Parameter rebor : ∀ E κ κ' P,
+    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
+  Parameter bor_unnest : ∀ E κ κ' P,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
+
+  Parameter 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.[κ]).
+  Parameter 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).
+  Parameter bor_acc_strong : ∀ E q κ P,
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
+      ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
+  Parameter bor_acc_atomic_strong : ∀ E κ P,
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
+      (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
+         ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+           ([†κ] ∗ |={E∖↑lftN,E}=> True).
+
+  (* Because Coq's module system is horrible, we have to repeat properties of lft_incl here
+     unless we want to prove them twice (both here and in model.primitive) *)
+  Parameter lft_le_incl : ∀ κ κ', κ' ⊆ κ → (κ ⊑ κ')%I.
+  Parameter lft_incl_refl : ∀ κ, (κ ⊑ κ)%I.
+  Parameter lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
+  Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
+  Parameter lft_incl_mono : ∀ κ1 κ1' κ2 κ2',
+    κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
+  Parameter lft_incl_acc : ∀ E κ κ' q,
+    ↑lftN ⊆ E → κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
+  Parameter lft_incl_dead : ∀ E κ κ', ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
+  Parameter lft_incl_intro : ∀ κ κ',
+    □ ((∀ 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_exists : ∀ {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+  Parameter bor_acc_atomic_cons : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
+      (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+      ([†κ] ∗ |={E∖↑lftN,E}=> True).
+  Parameter bor_acc_atomic : ∀ E κ P,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
+       (▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ &{κ}P)) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True).
+
+  End properties.
+End lifetime_sig.
diff --git a/theories/lifetime/accessors.v b/theories/lifetime/model/accessors.v
similarity index 94%
rename from theories/lifetime/accessors.v
rename to theories/lifetime/model/accessors.v
index 2f3b4b0381da371ff6ab9123ee76e34f6ee4d979..6b53811d3ff680b6877fb60f41b38364598a3d7a 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -255,18 +255,7 @@ Proof.
       iApply fupd_intro_mask'. solve_ndisj.
 Qed.
 
-Lemma bor_acc_cons E q κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
-    ∀ Q, ▷ Q -∗ ▷(▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
-Proof.
-  iIntros (?) "#LFT HP Htok".
-  iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
-  iIntros "!>*HQ HPQ". iMod ("Hclose" with "*HQ [HPQ]") as "[Hb $]".
-  - iNext. iIntros "? _". by iApply "HPQ".
-  - iApply (bor_shorten with "Hκκ' Hb").
-Qed.
-
+(* These derived lemmas are needed inside the model. *)
 Lemma bor_acc_atomic_cons E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
@@ -282,15 +271,6 @@ Proof.
   - iRight. by iFrame.
 Qed.
 
-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_cons with "LFT HP Htok") as "($ & Hclose)"; first done.
-  iIntros "!>HP". iMod ("Hclose" with "*HP []") as "[$ $]"; auto.
-Qed.
-
 Lemma bor_acc_atomic E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
@@ -301,4 +281,5 @@ Proof.
   - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "* HP []"); auto.
   - iRight. by iFrame.
 Qed.
+
 End accessors.
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/model/borrow.v
similarity index 99%
rename from theories/lifetime/borrow.v
rename to theories/lifetime/model/borrow.v
index 7ce44adae63e23c76305d04745456b27ef0f931e..4fba2a91f2ada9046e7430fd3c9887fe32e39711 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -182,4 +182,5 @@ Proof.
       iRight. iSplit; last by auto. iExists _. iFrame. }
     unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
 Qed.
+
 End borrow.
diff --git a/theories/lifetime/creation.v b/theories/lifetime/model/creation.v
similarity index 100%
rename from theories/lifetime/creation.v
rename to theories/lifetime/model/creation.v
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/model/definitions.v
similarity index 86%
rename from theories/lifetime/definitions.v
rename to theories/lifetime/model/definitions.v
index ce443fd3d3d9cafee71d341be36168e73fc3b969..97a5cde305b35e9e2d5d0d30269b4b24a4c9cd8b 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,65 +1,20 @@
-From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.prelude Require Export gmultiset strings.
-From iris.base_logic.lib Require Export invariants.
-From iris.base_logic.lib Require Import boxes.
+From iris.algebra Require Import csum auth frac agree gset.
 From iris.base_logic Require Import big_op.
+From iris.base_logic.lib Require Import boxes.
+From lrust.lifetime Require Export lifetime_sig.
 Set Default Proof Using "Type".
 Import uPred.
 
-Definition lftN : namespace := nroot .@ "lft".
-Definition borN : namespace := lftN .@ "bor".
-Definition inhN : namespace := lftN .@ "inh".
-Definition mgmtN : namespace := lftN .@ "mgmt".
-
-Definition atomic_lft := positive.
-Notation lft := (gmultiset positive).
-Definition static : lft := ∅.
-
-Inductive bor_state :=
-  | Bor_in
-  | Bor_open (q : frac)
-  | Bor_rebor (κ : lft).
-Instance bor_state_eq_dec : EqDecision bor_state.
-Proof. solve_decision. Defined.
-Canonical bor_stateC := leibnizC bor_state.
 
 Definition bor_filled (s : bor_state) : bool :=
   match s with Bor_in => true | _ => false end.
 
-Definition lft_stateR := csumR fracR unitR.
 Definition to_lft_stateR (b : bool) : lft_stateR :=
   if b then Cinl 1%Qp else Cinr ().
-
-Record lft_names := LftNames {
-  bor_name : gname;
-  cnt_name : gname;
-  inh_name : gname
-}.
-Instance lft_names_eq_dec : EqDecision lft_names.
-Proof. solve_decision. Defined.
-Canonical lft_namesC := leibnizC lft_names.
-
-Definition alftUR := gmapUR atomic_lft lft_stateR.
 Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
-
-Definition ilftUR := gmapUR lft (agreeR lft_namesC).
 Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
-
-Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
 Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
 
-Definition inhUR := gset_disjUR slice_name.
-
-Class lftG Σ := LftG {
-  lft_box :> boxG Σ;
-  alft_inG :> inG Σ (authR alftUR);
-  alft_name : gname;
-  ilft_inG :> inG Σ (authR ilftUR);
-  ilft_name : gname;
-  lft_bor_inG :> inG Σ (authR borUR);
-  lft_cnt_inG :> inG Σ (authR natUR);
-  lft_inh_inG :> inG Σ (authR inhUR);
-}.
 
 Section defs.
   Context `{invG Σ, lftG Σ}.
@@ -186,9 +141,9 @@ End defs.
 Instance: Params (@lft_bor_alive) 4.
 Instance: Params (@lft_inh) 5.
 Instance: Params (@lft_vs) 4.
-Instance: Params (@idx_bor) 5.
-Instance: Params (@raw_bor) 4.
-Instance: Params (@bor) 4.
+Instance idx_bor_params : Params (@idx_bor) 5.
+Instance raw_bor_params : Params (@raw_bor) 4.
+Instance bor_params : Params (@bor) 4.
 
 Notation "q .[ κ ]" := (lft_tok q κ)
     (format "q .[ κ ]", at level 0) : uPred_scope.
@@ -201,6 +156,9 @@ Notation "&{ κ , i } P" := (idx_bor κ i P)
 
 Infix "⊑" := lft_incl (at level 70) : uPred_scope.
 
+(* TODO: Making all these things opaque is rather annoying, we should
+   find a way to avoid it, or *at least*, to avoid having to manually unfold
+   this because iDestruct et al don't look through these names any more. *)
 Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   lft_inh lft_inv_alive lft_vs_inv lft_vs lft_inv_dead lft_inv lft_incl
   idx_bor_own idx_bor raw_bor bor.
@@ -307,8 +265,8 @@ Proof. rewrite /lft_tok. apply _. Qed.
 
 Global Instance lft_dead_persistent κ : PersistentP [†κ].
 Proof. rewrite /lft_dead. apply _. Qed.
-Global Instance lft_dead_timeless κ : PersistentP [†κ].
-Proof. rewrite /lft_tok. apply _. Qed.
+Global Instance lft_dead_timeless κ : TimelessP [†κ].
+Proof. rewrite /lft_dead. apply _. Qed.
 
 Global Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
 Proof. rewrite /lft_incl. apply _. Qed.
diff --git a/theories/lifetime/faking.v b/theories/lifetime/model/faking.v
similarity index 98%
rename from theories/lifetime/faking.v
rename to theories/lifetime/model/faking.v
index 1def1f51ec0e86b8774c3613d5437f0700d47c11..07e170e125ae4f9532bc06b80755c289916caee6 100644
--- a/theories/lifetime/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -112,8 +112,7 @@ Proof.
 Qed.
 
 Lemma bor_fake E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
+  ↑lftN ⊆ E → lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
 Proof.
   iIntros (?) "#LFT H†". iMod (raw_bor_fake' with "LFT H†"); first done.
   iModIntro. unfold bor. iExists κ. iFrame. iApply lft_incl_refl.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/model/primitive.v
similarity index 98%
rename from theories/lifetime/primitive.v
rename to theories/lifetime/model/primitive.v
index 7ed8780ac6c7e700fa276a22abff64e1fa2547b4..4832b7684bd5539a2f29060bba10e69544b20db0 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export definitions.
+From lrust.lifetime.model Require Export definitions.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes fractional.
@@ -353,6 +353,12 @@ Proof.
   iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
 Qed.
 
+Lemma lft_incl_intro κ κ' :
+  □ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
+               lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
+      (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
+Proof. reflexivity. Qed.
+
 (** Basic rules about borrows *)
 Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
 Proof.
@@ -363,7 +369,7 @@ Proof.
     iExists κ'. iFrame. iExists s. by iFrame.
 Qed.
 
-Lemma bor_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
+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κκ'").
diff --git a/theories/lifetime/raw_reborrow.v b/theories/lifetime/model/raw_reborrow.v
similarity index 100%
rename from theories/lifetime/raw_reborrow.v
rename to theories/lifetime/model/raw_reborrow.v
diff --git a/theories/lifetime/reborrow.v b/theories/lifetime/model/reborrow.v
similarity index 88%
rename from theories/lifetime/reborrow.v
rename to theories/lifetime/model/reborrow.v
index 567d6b42ce593246b5f0d4e8c61a1c6c23245c83..59d91f255dc536493ab7b14beb24f237b9ed25ab 100644
--- a/theories/lifetime/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export borrow derived.
+From lrust.lifetime Require Export borrow.
 From lrust.lifetime Require Import raw_reborrow accessors.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
@@ -10,6 +10,18 @@ Section reborrow.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
+(* This lemma has no good place... and reborrowing is where we need it inside the model. *)
+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_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
+  - iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
+    iExists x. iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
+  - iExists inhabitant. by iApply (bor_fake with "LFT").
+Qed.
+
 Lemma rebor E κ κ' P :
   ↑lftN ⊆ E →
   lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index 41a69f9e11845696b3a59b32397df9a86ef0b838..d61bac2c178ca6a9a5ba1fc4edb0e591cb56c265 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export derived.
+From lrust.lifetime Require Export lifetime.
 From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
diff --git a/theories/lifetime/shr_borrow.v b/theories/lifetime/shr_borrow.v
index 10a1473121b6cefac1c855f5d4b0160c1d9d2cb9..2e1975771a4843bde31af5d3d1360dfbbd7d3b29 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 lifetime.
 Set Default Proof Using "Type".
 
 (** Shared bors  *)
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index e105e2cdf43c26f9076dd432451a953a50d48040..837756bb8e7c6f08b68a8f6a4f80fe014f9f53c9 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -1,6 +1,5 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lifetime Require Import reborrow frac_borrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export uniq_bor shr_bor own.
 From lrust.typing Require Import lft_contexts type_context programs.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 853194869fe7717165c38e0eab5fe20a54e40d0d..3d4398a37aebaa8d4173d8cf9f2f62af2ac65c6e 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -1,6 +1,5 @@
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
 Set Default Proof Using "Type".
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index e239890bec89a9ee6fe241b53b3d8bd9019bd4f2..67c01c7d50a62ed3832bc63607165243b16cc4b8 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -1,7 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Import notation.
-From lrust.lifetime Require Import definitions.
 From lrust.typing Require Import type lft_contexts type_context.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index c8ca59f84fedddedd5efcb55c7add62bde7eb86a..140ad5f141f7d1ce5f20a1c09e2efa315fbf949d 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -1,4 +1,3 @@
-From lrust.lifetime Require Import definitions.
 From lrust.typing Require Export lft_contexts type bool.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 709fe8b854ef0ad2aad7118e677ce7a1cab3629f..81079cef6de55148bfd366f9433291ad04cf5908 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -1,7 +1,6 @@
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import vector.
-From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs cont.
 Set Default Proof Using "Type".
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 1fa4444ea08554e2900355c3c41da5fb44dbb67e..eec88edf6202ba2f77ae69e79052ea0e12812a21 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import fractional.
-From lrust.lifetime Require Import derived borrow frac_borrow.
+From lrust.lifetime Require Import frac_borrow.
 Set Default Proof Using "Type".
 
 Inductive elctx_elt : Type :=
diff --git a/theories/typing/own.v b/theories/typing/own.v
index c095a2a744bbb9c975d011760e83795b8213fdb3..9637508da28f9aa861ff81a7bc06e12b676e07a5 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -1,7 +1,6 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.lang Require Export new_delete.
 From lrust.lang Require Import memcpy.
 From lrust.typing Require Export type.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index bed771821285edbe01b9f095f8eefdcc0e8422d6..f91ba5cd359b372c0c74296b445ffed2e38ac75e 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -1,6 +1,5 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import list.
-From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index b02d8d1d01747b079250786b47b4db983107303f..e6beb9f444a7f339b9234c9234690bda17632b29 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -1,7 +1,6 @@
 From Coq Require Import Qcanon.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import type_context lft_contexts product own uniq_bor shr_bor.
 Set Default Proof Using "Type".
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 4ff553ea16b297b1309506047d6864d68d4661f8..97b24c7f324e0840523ac3aa77f80b6669695e01 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,7 +1,6 @@
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Export notation.
 From lrust.lang Require Import proofmode memcpy.
-From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 23350e748c6ece89fb43c1bc7da2800f8d63ace0..9aef143a737a02ae7a8695e05fd95c5e825240d7 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -1,6 +1,5 @@
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-From lrust.lifetime Require Import frac_borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import lft_contexts type_context programs.
 Set Default Proof Using "Type".
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 330da63da8a2e96d3fe4f59fcfc16e3c2d79b9d6..e42e2536f173cfdf302d3d9567d4d70d0a7ed285 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -1,7 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import list.
 From iris.base_logic Require Import fractional.
-From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export type.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index d770fb2a7fa3cada4b3ff1ad947b2669d2a5f679..0d670d2336efd87c4d8c452c4ab967638871633f 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -1,4 +1,3 @@
-From lrust.lifetime Require Import definitions.
 From lrust.lang Require Import new_delete.
 From lrust.typing Require Import programs product product_split own uniq_bor
                     shr_bor int function lft_contexts uninit cont.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 8585d23063dbb300f9fabd75ff29490829fa9e61..5e0d853a9f77ecf4da273a27ebc2699859533f59 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export na_invariants.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Export proofmode notation.
-From lrust.lifetime Require Import borrow frac_borrow reborrow.
+From lrust.lifetime Require Export frac_borrow.
 From lrust.typing Require Import lft_contexts.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 741e0558253374799e280d8525c4d125f1aa6cc9..e76368fa665db6391ae5337f498b5280a796ac6b 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -1,7 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Import notation.
-From lrust.lifetime Require Import definitions.
 From lrust.typing Require Import type lft_contexts.
 Set Default Proof Using "Type".
 
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index eece54ef7b85f885d1f285bfc810caae8e1015e0..71f22b6dee74c070bae7340384ff6ec570331129 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -1,6 +1,5 @@
 From iris.proofmode Require Import tactics.
 From lrust.lang Require Import heap memcpy.
-From lrust.lifetime Require Import borrow frac_borrow.
 From lrust.typing Require Export uninit uniq_bor shr_bor own sum.
 From lrust.typing Require Import lft_contexts type_context programs product.
 Set Default Proof Using "Type".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 8c776efa2fcffc5bb6abe2b9234bf067bc66508d..74d96144d0859ab58907f61d798de7e7414543b6 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -1,6 +1,5 @@
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
-From lrust.lifetime Require Import borrow frac_borrow reborrow.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
 From lrust.typing Require Import lft_contexts type_context shr_bor programs.