diff --git a/_CoqProject b/_CoqProject
index a8fc54505804bfc0f6db4864fab9ec08bb1db55f..8448ae4c2752ca37c2a2a25b439f6705e2cec442 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,21 +1,27 @@
 -Q theories lrust
-theories/adequacy.v
-theories/derived.v
-theories/heap.v
-theories/lang.v
-theories/lifting.v
-theories/memcpy.v
-theories/notation.v
-theories/proofmode.v
-theories/races.v
-theories/tactics.v
-theories/wp_tactics.v
-theories/lifetime.v
-theories/tl_borrow.v
-theories/shr_borrow.v
-theories/frac_borrow.v
-theories/type.v
-theories/type_incl.v
-theories/perm.v
-theories/perm_incl.v
-theories/typing.v
+theories/lifetime/definitions.v
+theories/lifetime/derived.v
+theories/lifetime/creation.v
+theories/lifetime/primitive.v
+theories/lifetime/accessors.v
+theories/lifetime/borrow.v
+theories/lifetime/rebor.v
+theories/lifetime/shr_borrow.v
+theories/lifetime/frac_borrow.v
+theories/lifetime/tl_borrow.v
+theories/lang/adequacy.v
+theories/lang/derived.v
+theories/lang/heap.v
+theories/lang/lang.v
+theories/lang/lifting.v
+theories/lang/memcpy.v
+theories/lang/notation.v
+theories/lang/proofmode.v
+theories/lang/races.v
+theories/lang/tactics.v
+theories/lang/wp_tactics.v
+theories/typing/type.v
+theories/typing/type_incl.v
+theories/typing/perm.v
+theories/typing/perm_incl.v
+theories/typing/typing.v
diff --git a/theories/adequacy.v b/theories/lang/adequacy.v
similarity index 92%
rename from theories/adequacy.v
rename to theories/lang/adequacy.v
index e5c53aef9a295b29a269e00b377c3b737a9fe60d..0189938398f2dbc58668dc9107b832bed0527186 100644
--- a/theories/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export hoare adequacy.
-From lrust Require Export heap.
 From iris.algebra Require Import auth.
-From lrust Require Import proofmode notation.
+From lrust.lang Require Export heap.
+From lrust.lang Require Import proofmode notation.
 
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> irisPreG lrust_lang Σ;
diff --git a/theories/derived.v b/theories/lang/derived.v
similarity index 98%
rename from theories/derived.v
rename to theories/lang/derived.v
index 1a2180deea64c381d029206151e663d689430993..f44b27824a057c43d5546b9334428979249a91d2 100644
--- a/theories/derived.v
+++ b/theories/lang/derived.v
@@ -1,4 +1,4 @@
-From lrust Require Export lifting.
+From lrust.lang Require Export lifting.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
diff --git a/theories/heap.v b/theories/lang/heap.v
similarity index 99%
rename from theories/heap.v
rename to theories/lang/heap.v
index dbe54f5eaef42f33da9cedf4d8cd42159c0237c1..9289944881bb346bb25bc2d95f47e1123dff21db 100644
--- a/theories/heap.v
+++ b/theories/lang/heap.v
@@ -2,7 +2,7 @@ From iris.algebra Require Import cmra_big_op gmap frac dec_agree.
 From iris.algebra Require Import csum excl auth.
 From iris.base_logic Require Import big_op lib.invariants lib.fractional.
 From iris.proofmode Require Export tactics.
-From lrust Require Export lifting.
+From lrust.lang Require Export lifting.
 Import uPred.
 
 Definition heapN : namespace := nroot .@ "heap".
@@ -69,10 +69,9 @@ Section definitions.
   Proof. apply _. Qed.
 End definitions.
 
-Typeclasses Opaque heap_ctx heap_mapsto heap_freeable.
+Typeclasses Opaque heap_ctx heap_mapsto heap_freeable heap_mapsto_vec.
 Instance: Params (@heap_mapsto) 4.
 Instance: Params (@heap_freeable) 5.
-Instance: Params (@heap_ctx) 2.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
@@ -128,7 +127,7 @@ Section heap.
   Proof. done. Qed.
 
   Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦∗{q} vl).
-  Proof. apply _. Qed.
+  Proof. rewrite /heap_mapsto_vec. apply _. Qed.
 
   Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
   Proof.
diff --git a/theories/lang.v b/theories/lang/lang.v
similarity index 100%
rename from theories/lang.v
rename to theories/lang/lang.v
diff --git a/theories/lifting.v b/theories/lang/lifting.v
similarity index 98%
rename from theories/lifting.v
rename to theories/lang/lifting.v
index 4fead4c2ce18f526efcbda81e9a51528f48e79fa..a0fc74912e16d223de9c322b9aedb5fa886a60b8 100644
--- a/theories/lifting.v
+++ b/theories/lang/lifting.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import ectx_lifting.
-From lrust Require Export lang.
-From lrust Require Import tactics.
+From lrust.lang Require Export lang.
+From lrust.lang Require Import tactics.
 From iris.proofmode Require Import tactics.
 Import uPred.
 Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
diff --git a/theories/memcpy.v b/theories/lang/memcpy.v
similarity index 94%
rename from theories/memcpy.v
rename to theories/lang/memcpy.v
index e945532fe282f8afd8951121fe4b6157cf8ddbb1..7c42700673bbcffe528937237f632c76f2ca6dfb 100644
--- a/theories/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Import namespaces.
-From lrust Require Export notation.
-From lrust Require Import heap proofmode.
+From lrust.lang Require Export notation.
+From lrust.lang Require Import heap proofmode.
 
 Definition memcpy : val :=
   rec: "memcpy" ["dst";"len";"src"] :=
diff --git a/theories/notation.v b/theories/lang/notation.v
similarity index 98%
rename from theories/notation.v
rename to theories/lang/notation.v
index f60e5d3cb3309d12cf7cc4838d37385dd148ddb4..719f38bd50dc29696270886fe743092d877986e6 100644
--- a/theories/notation.v
+++ b/theories/lang/notation.v
@@ -1,4 +1,4 @@
-From lrust Require Export derived.
+From lrust.lang Require Export derived.
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
diff --git a/theories/proofmode.v b/theories/lang/proofmode.v
similarity index 91%
rename from theories/proofmode.v
rename to theories/lang/proofmode.v
index dbd10fe695c5eca23088bfa4f57ee6822605890d..fb4d20e89692e4758c5581b997e1d180e304ea3e 100644
--- a/theories/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.base_logic Require Import namespaces.
-From lrust Require Export wp_tactics heap.
+From lrust.lang Require Export wp_tactics heap.
 Import uPred.
 
 Ltac wp_strip_later ::= iNext.
@@ -14,7 +14,7 @@ Implicit Types Δ : envs (iResUR Σ).
 
 Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → 0 < n →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   (∀ l vl, n = length vl → ∃ Δ'',
     envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
       = Some Δ'' ∧
@@ -23,7 +23,7 @@ Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
 Proof.
   intros ???? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
   rewrite -always_and_sep_l. apply and_intro; first done.
-  rewrite into_later_env_sound; apply later_mono, forall_intro=> l;
+  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l;
   apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
   apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
   destruct (HΔ l vl) as (Δ''&?&HΔ'). done.
@@ -32,7 +32,7 @@ Qed.
 
 Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → n = length vl →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
   envs_delete i1 false Δ' = Δ'' →
   envs_lookup i2 Δ'' = Some (false, †l…n')%I →
@@ -44,13 +44,13 @@ Proof.
   intros ?? -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
   eapply wand_apply; first exact:wp_free. rewrite -!assoc -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound -!later_sep; apply later_mono.
+  rewrite into_laterN_env_sound -!later_sep; apply later_mono.
   do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True.
 Qed.
 
 Lemma tac_wp_read Δ Δ' E i l q v o Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   (Δ' ⊢ |={E}=> Φ v) →
   Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
@@ -58,18 +58,18 @@ Proof.
   intros ??[->| ->]???.
   - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_na.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
+    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
       by apply later_mono, sep_mono_r, wand_mono.
   - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_sc.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
+    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
       by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
   to_val e = Some v' →
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
   (Δ'' ⊢ |={E}=> Φ (LitV LitUnit)) →
@@ -78,14 +78,13 @@ Proof.
   intros ???[->| ->]????.
   - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_na.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
   - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_sc.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
-
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
diff --git a/theories/races.v b/theories/lang/races.v
similarity index 99%
rename from theories/races.v
rename to theories/lang/races.v
index c7273d30e8ce9a6749e72fb08c99926b1cc3ea51..439161514d8d5d0f2a5031c2b743ab74d2b6db2a 100644
--- a/theories/races.v
+++ b/theories/lang/races.v
@@ -1,7 +1,7 @@
+From iris.prelude Require Import gmap.
 From iris.program_logic Require Export hoare.
 From iris.program_logic Require Import adequacy.
-From lrust Require Import tactics.
-From iris.prelude Require Import gmap.
+From lrust.lang Require Import tactics.
 
 Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
 
diff --git a/theories/tactics.v b/theories/lang/tactics.v
similarity index 99%
rename from theories/tactics.v
rename to theories/lang/tactics.v
index 91bdc55c60f2d6f96cbcf3cc92087bac4dc06b9c..21e3309ba8c83e4f188836669ef099d0fa920f04 100644
--- a/theories/tactics.v
+++ b/theories/lang/tactics.v
@@ -1,5 +1,5 @@
-From lrust Require Export lang.
 From iris.prelude Require Import fin_maps.
+From lrust.lang Require Export lang.
 
 (** We define an alternative representation of expressions in which the
 embedding of values and closed expressions is explicit. By reification of
diff --git a/theories/wp_tactics.v b/theories/lang/wp_tactics.v
similarity index 98%
rename from theories/wp_tactics.v
rename to theories/lang/wp_tactics.v
index 0775226d94c4be664d143af37e3941ff34253e64..0d136c4826ebfb35ab5c9157f5e0521b5bd3dd5d 100644
--- a/theories/wp_tactics.v
+++ b/theories/lang/wp_tactics.v
@@ -1,4 +1,4 @@
-From lrust Require Export tactics derived.
+From lrust.lang Require Export tactics derived.
 Import uPred.
 
 (** wp-specific helper tactics *)
diff --git a/theories/lft_contexts.v b/theories/lft_contexts.v
deleted file mode 100644
index 1f78d25a05f871297b04d1f91eecab7feea52964..0000000000000000000000000000000000000000
--- a/theories/lft_contexts.v
+++ /dev/null
@@ -1,20 +0,0 @@
-From iris.proofmode Require Import tactics.
-From lrust Require Export type lifetime.
-
-Section lft_contexts.
-
-  Context `{iris_typeG Σ}.
-
-  Inductive ext_lft_ctx_elt :=
-  | 
-
-  Definition ext_lft_ctx := Qp → iProp Σ.
-
-  Global Instance empty_ext_lft_ctx : Empty ext_lft_ctx := λ _, True%I.
-
-  
-
-
-  Definition int_lft_ctx := iProp Σ.
-
-  
\ No newline at end of file
diff --git a/theories/lifetime.v b/theories/lifetime.v
deleted file mode 100644
index 3f4cbe57a9667a0323ff0f6b287655d8a125ed18..0000000000000000000000000000000000000000
--- a/theories/lifetime.v
+++ /dev/null
@@ -1,336 +0,0 @@
-From iris.algebra Require Import csum auth frac gmap.
-From iris.base_logic.lib Require Export fancy_updates invariants namespaces.
-From iris.base_logic.lib Require Export fractional.
-From iris.proofmode Require Import tactics.
-
-Definition lftN := nroot .@ "lft".
-Definition atomic_lft := positive.
-
-Definition lft_tokUR : ucmraT :=
-  authUR (gmapUR atomic_lft (csumR fracR unitR)).
-
-(* FIXME : this is not the actual definitions. *)
-Definition borrow_idx := positive.
-Definition borrow_tokUR : ucmraT :=
-  authUR (gmapUR borrow_idx fracR).
-
-Class lifetimeG Σ := LifetimeG {
-  lft_tok_inG :> inG Σ lft_tokUR;
-  borrow_tok_inG :> inG Σ borrow_tokUR;
-  lft_toks_name : gname;
-  borrow_tok_name : gname
-}.
-
-Parameter lft_ctx : ∀ `{lifetimeG Σ}, iProp Σ.
-
-Section defs.
-
-  (*** Definitions  *)
-
-  Context `{lifetimeG Σ}.
-
-  Definition lifetime := gmap atomic_lft nat.
-
-  Definition static : lifetime := ∅.
-
-  Definition Qp_nat_mul  (q : Qp) (n : nat) : option Qp :=
-    match n with
-    | O => None
-    | S n' => Some (Nat.iter n' (λ acc, q ⋅ acc)%Qp q)
-    end.
-
-  Definition lft_own (q : Qp) (κ : lifetime) : iProp Σ :=
-    own lft_toks_name (◯ (Cinl <$> omap (Qp_nat_mul q) κ)).
-
-  Definition lft_dead (κ : lifetime) : iProp Σ :=
-    (∃ Λ, ⌜∃ n, κ !! Λ = Some (S n)⌝ ∗
-            own lft_toks_name (◯ {[ Λ := Cinr () ]}))%I.
-
-  Definition idx_borrow_own (q : Qp) (i : borrow_idx) :=
-    own borrow_tok_name (◯ {[ i := q ]}).
-
-  Parameter idx_borrow:
-    ∀ `{lifetimeG Σ} (κ : lifetime) (i : borrow_idx) (P : iProp Σ), iProp Σ.
-
-  Definition borrow (κ : lifetime) (P : iProp Σ) : iProp Σ :=
-    (∃ i, idx_borrow κ i P ∗ idx_borrow_own 1 i)%I.
-
-End defs.
-
-Typeclasses Opaque lft_own lft_dead borrow.
-
-(*** Notations  *)
-
-Notation "q .[ κ ]" := (lft_own q κ)
-    (format "q .[ κ ]", at level 0): uPred_scope.
-Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
-Notation "&{ κ } P" := (borrow κ P)
-  (format "&{ κ } P", at level 20, right associativity) : uPred_scope.
-Hint Unfold lifetime : typeclass_instances.
-
-Section lft.
-  Context `{invG Σ, lifetimeG Σ}.
-
-  Axiom lft_ctx_alloc : (|={∅}=> lft_ctx)%I.
-
-  (*** PersitentP, TimelessP, Proper and Fractional instances  *)
-
-  Global Instance lft_own_timeless q κ : TimelessP q.[κ].
-  Proof. unfold lft_own. apply _. Qed.
-  Global Instance lft_own_fractional κ : Fractional (λ q, q.[κ])%I.
-  Proof.
-    intros p q. rewrite /lft_own -own_op -auth_frag_op.
-    f_equiv. constructor. done. simpl. intros Λ.
-    rewrite lookup_op !lookup_fmap !lookup_omap. apply reflexive_eq.
-    case: (κ !! Λ)=>[[|a]|]//=. rewrite -Some_op Cinl_op. repeat f_equal.
-    induction a as [|a IH]. done.
-    rewrite /= IH /op /cmra_op /= /frac_op !assoc. f_equal.
-    rewrite -!assoc. f_equal. apply (comm _).
-  Qed.
-  Global Instance lft_own_as_fractional κ q :
-    AsFractional q.[κ] (λ q, q.[κ])%I q.
-  Proof. done. Qed.
-
-  Global Instance lft_dead_persistent κ : PersistentP [†κ].
-  Proof. unfold lft_dead. apply _. Qed.
-  Global Instance lft_dead_timeless κ : PersistentP [†κ].
-  Proof. unfold lft_dead. apply _. Qed.
-
-  Axiom idx_borrow_persistent :
-    ∀ κ i P, PersistentP (idx_borrow κ i P).
-  Global Existing Instance idx_borrow_persistent.
-  Axiom idx_borrow_proper :
-    ∀ κ i, Proper ((⊣⊢) ==> (⊣⊢)) (idx_borrow κ i).
-  Global Existing Instance idx_borrow_proper.
-
-  Axiom idx_borrow_own_timeless :
-    ∀ q i, TimelessP (idx_borrow_own q i).
-  Global Existing Instance idx_borrow_own_timeless.
-
-  Global Instance borrow_proper κ: Proper ((⊣⊢) ==> (⊣⊢)) (borrow κ).
-  Proof. solve_proper. Qed.
-
-  Axiom lft_ctx_persistent : PersistentP lft_ctx.
-
-  (** Basic rules about lifetimes  *)
-  Lemma lft_own_op q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⋅ κ2].
-  Proof.
-    rewrite /lft_own -own_op. f_equiv. constructor. done. move=>Λ /=.
-    rewrite lookup_op !lookup_fmap !lookup_omap lookup_op.
-    case: (κ1 !! Λ)=>[[|a1]|]; case: (κ2 !! Λ)=>[[|a2]|]/=; rewrite ?right_id ?left_id //.
-    apply reflexive_eq. apply (f_equal (Some ∘ Cinl)).
-    induction a1. done. rewrite /= -assoc. by f_equal.
-  Qed.
-
-  Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [† κ1⋅κ2].
-  Proof.
-    unfold lft_dead. setoid_rewrite lookup_op. iSplit.
-    - iIntros "[H|H]"; iDestruct "H" as (Λ) "[H?]";
-        iDestruct "H" as %[n Hn]; iExists _; iFrame; iPureIntro; rewrite Hn.
-      + case: (κ2 !! Λ); eauto.
-      + case: (κ1 !! Λ)=>[n'|]; eauto. exists (n' + n)%nat. by apply (f_equal Some).
-    - iIntros "H". iDestruct "H" as (Λ) "[H Hown]"; eauto. iDestruct "H" as %[n Hn].
-      case K1: (κ1 !! Λ) Hn=>[[|a1]|]; case K2: (κ2 !! Λ)=>[[|a2]|]; intros [=<-];
-      (iRight + iLeft); iExists Λ; iIntros "{$Hown}!%"; by eauto.
-  Qed.
-
-  Axiom lft_create :
-    ∀ `(↑lftN ⊆ E),
-      lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
-
-  Axiom idx_borrow_acc :
-    ∀ `(↑lftN ⊆ E) q κ i P,
-      lft_ctx -∗ idx_borrow κ i P -∗ idx_borrow_own 1 i
-              -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ idx_borrow_own 1 i ∗ q.[κ]).
-  Axiom idx_borrow_atomic_acc :
-    ∀ `(↑lftN ⊆ E) q κ i P,
-      lft_ctx -∗ idx_borrow κ i P -∗ idx_borrow_own q i
-         ={E,E∖↑lftN}=∗
-            ▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_borrow_own q i) ∨
-            [†κ] ∗ (|={E∖↑lftN,E}=> idx_borrow_own q i).
-
-  (** Basic borrows  *)
-  Axiom borrow_create :
-    ∀ `(↑lftN ⊆ E) κ P, lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
-  Axiom borrow_fake : ∀ `(↑lftN ⊆ E) κ P, lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
-  Axiom borrow_split :
-    ∀ `(↑lftN ⊆ E) κ P Q, lft_ctx -∗ &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
-  Axiom borrow_combine :
-    ∀ `(↑lftN ⊆ E) κ P Q, lft_ctx -∗ &{κ}P -∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
-  Axiom borrow_acc_strong :
-    ∀ `(↑lftN ⊆ E) q κ P,
-      lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗
-      ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ ↑lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
-  Axiom borrow_acc_atomic_strong :
-    ∀ `(↑lftN ⊆ E) κ P,
-      lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
-        (▷ P ∗ ∀ Q, ▷ Q ∗ ▷([†κ] -∗ ▷Q ={⊤ ∖ ↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ}Q) ∨
-        [†κ] ∗ |={E∖↑lftN,E}=> True.
-  Axiom borrow_reborrow' :
-    ∀ `(↑lftN ⊆ E) κ κ' P, κ ≼ κ' →
-      lft_ctx -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
-  Axiom borrow_unnest :
-    ∀ `(↑lftN ⊆ E) κ κ' P, lft_ctx -∗ &{κ'}&{κ}P ={E, E∖↑lftN}▷=∗ &{κ ⋅ κ'}P.
-
-  (*** Derived lemmas  *)
-
-  Lemma lft_own_dead q κ : q.[κ] -∗ [† κ] -∗ False.
-  Proof.
-    rewrite /lft_own /lft_dead.
-    iIntros "Hl Hr". iDestruct "Hr" as (Λ) "[HΛ Hr]".
-    iDestruct "HΛ" as %[n HΛ].
-    iDestruct (own_valid_2 with "Hl Hr") as %Hval. iPureIntro.
-    generalize (Hval Λ).
-    by rewrite lookup_op lookup_singleton lookup_fmap lookup_omap HΛ.
-  Qed.
-
-  Lemma lft_own_static q : (|==> q.[static])%I.
-  Proof.
-    rewrite /lft_own /static omap_empty fmap_empty.
-    apply (own_empty lft_tokUR lft_toks_name).
-  Qed.
-
-  Lemma lft_not_dead_static : [† static] -∗ False.
-  Proof.
-    rewrite /lft_dead /static. setoid_rewrite lookup_empty.
-    iIntros "HΛ". iDestruct "HΛ" as (Λ) "[% _]". naive_solver.
-  Qed.
-
-  Global Instance into_and_lft_own κ1 κ2 q :
-    IntoAnd false q.[κ1⋅κ2] q.[κ1] q.[κ2].
-  Proof. by rewrite /IntoAnd lft_own_op. Qed.
-
-  Global Instance from_sep_lft_own κ1 κ2 q :
-    FromSep q.[κ1⋅κ2] q.[κ1] q.[κ2].
-  Proof. by rewrite /FromSep lft_own_op. Qed.
-
-  Lemma borrow_acc E q κ P :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
-  Proof.
-    iIntros (?) "#LFT HP Htok".
-    iMod (borrow_acc_strong with "LFT HP Htok") as "[HP Hclose]". done.
-    iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>_$".
-  Qed.
-
-  Lemma borrow_exists {A} E κ (Φ : A → iProp Σ) {_:Inhabited A}:
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
-  Proof.
-    iIntros (?) "#LFT Hb".
-    iMod (borrow_acc_atomic_strong with "LFT Hb") as "[[HΦ Hclose]|[H† Hclose]]". done.
-    - iDestruct "HΦ" as (x) "HΦ". iExists x. iApply "Hclose". iIntros "{$HΦ}!>_?". eauto.
-    - iMod "Hclose" as "_". iExists inhabitant. by iApply (borrow_fake with "LFT").
-  Qed.
-
-  Lemma borrow_or E κ P Q:
-    ↑lftN ⊆ E → lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
-  Proof.
-    iIntros (?) "#LFT H". rewrite uPred.or_alt.
-    iMod (borrow_exists with "LFT H") as ([]) "H"; auto.
-  Qed.
-
-  Lemma borrow_persistent E `{PersistentP _ P} κ q:
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
-  Proof.
-    iIntros (?) "#LFT Hb Htok".
-    iMod (borrow_acc with "LFT Hb Htok") as "[#HP Hob]". done.
-    by iMod ("Hob" with "HP") as "[_$]".
-  Qed.
-
-End lft.
-
-Typeclasses Opaque borrow.
-
-(*** Inclusion and shortening. *)
-
-Definition lft_incl `{invG Σ, lifetimeG Σ} κ κ' : iProp Σ :=
-  (□((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
-     ([†κ'] ={↑lftN}=∗ [†κ])))%I.
-
-Infix "⊑" := lft_incl (at level 60) : uPred_scope.
-
-Section incl.
-  Context `{invG Σ, lifetimeG Σ}.
-
-  Global Instance lft_incl_persistent κ κ': PersistentP (κ ⊑ κ') := _.
-
-  Lemma lft_incl_acc E κ κ' q:
-    ↑lftN ⊆ E →
-    κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
-  Proof.
-    iIntros (?) "#[H _] Hq". iApply fupd_mask_mono. eassumption.
-    iMod ("H" with "*Hq") as (q') "[Hq' Hclose]". iExists q'.
-    iIntros "{$Hq'}!>Hq". iApply fupd_mask_mono. eassumption. by iApply "Hclose".
-  Qed.
-
-  Lemma lft_incl_dead E κ κ': ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
-  Proof.
-    iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono. eassumption. by iApply "H".
-  Qed.
-
-  Lemma lft_le_incl κ κ': κ' ≼ κ → (κ ⊑ κ')%I.
-  Proof.
-    iIntros ([κ0 ->%leibniz_equiv]) "!#". iSplitR.
-    - iIntros (q) "[Hκ' Hκ0]". iExists q. iIntros "!>{$Hκ'}Hκ'!>". by iSplitR "Hκ0".
-    - iIntros "?!>". iApply lft_dead_or. auto.
-  Qed.
-
-  Lemma lft_incl_refl κ : (κ ⊑ κ)%I.
-  Proof. by apply lft_le_incl. Qed.
-
-  Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
-  Proof.
-    unfold lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
-    - iIntros (q) "Hκ".
-      iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
-      iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
-      iExists q''. iIntros "{$Hκ''}!>Hκ''". iMod ("Hclose'" with "Hκ''") as "Hκ'".
-        by iApply "Hclose".
-    - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
-  Qed.
-
-  Axiom idx_borrow_shorten :
-    ∀ κ κ' i P, κ ⊑ κ' -∗ idx_borrow κ' i P -∗ idx_borrow κ i P.
-
-  Lemma borrow_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
-  Proof.
-    iIntros "H⊑ H". unfold borrow. iDestruct "H" as (i) "[??]".
-    iExists i. iFrame. by iApply (idx_borrow_shorten with "H⊑").
-  Qed.
-
-  Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⋅ κ''.
-  Proof.
-    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_own_op.
-      iDestruct "Hκ'" as "[$ Hκ']". iDestruct "Hκ''" as "[$ Hκ'']".
-      iIntros "!>[Hκ'0 Hκ''0]". iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
-      by iMod ("Hclose''" with "[$Hκ'' $Hκ''0]") as "$".
-    - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
-  Qed.
-
-  Lemma lft_incl_static κ : (κ ⊑ static)%I.
-  Proof.
-    iIntros "!#". iSplitR.
-    - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_own_static. auto.
-    - iIntros "?". by iDestruct (lft_not_dead_static with "[-]") as "[]".
-  Qed.
-
-  Lemma reborrow E P κ κ':
-    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗  &{κ}P).
-  Proof.
-    iIntros (?) "#LFT #H⊑ HP".
-    iMod (borrow_reborrow' with "LFT HP") as "[Hκ' H∋]". done. by exists κ'.
-    iDestruct (borrow_shorten with "[H⊑] Hκ'") as "$".
-    { iApply (lft_incl_lb with "[] []"). done. iApply lft_incl_refl. }
-    iIntros "!>Hκ'". iApply ("H∋" with "[Hκ']"). iApply lft_dead_or. auto.
-  Qed.
-
-End incl.
-
-Typeclasses Opaque lft_incl.
diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
new file mode 100644
index 0000000000000000000000000000000000000000..cf8c06d846ca801ff3f80c5946cf5dfa3d62ef3a
--- /dev/null
+++ b/theories/lifetime/accessors.v
@@ -0,0 +1,298 @@
+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 -∗
+  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 (slice_empty _ _ true 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 (slice_fill _ _ true 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 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, idx_bor_own. iIntros (HE) "#LFT [#Hle #Hs] Hbor".
+  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_inv_alive_unfold.
+  iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
+  - iLeft. iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
+    unfold lft_bor_alive.
+    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 (slice_empty _ _ true with "Hs Hbox") as "[$ Hbox]".
+      solve_ndisj. by rewrite lookup_fmap EQB.
+    iMod fupd_intro_mask' as "Hclose"; last iIntros "!>HP". solve_ndisj.
+    iMod "Hclose" as "_". iMod (slice_fill _ _ true with "Hs HP Hbox") as "Hbox".
+      solve_ndisj. by rewrite lookup_insert. iFrame.
+    iApply "Hclose'". iExists _, _. iFrame. rewrite big_sepS_later.
+    iApply "Hclose''". iLeft. iFrame "%". iExists _, _. iFrame.
+    iExists _. iFrame.
+    rewrite insert_insert -(fmap_insert _ _ _ Bor_in) insert_id //.
+  - 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.
+  unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
+  iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(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 _ _ (κ'', s'') 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. }
+    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 (slice_delete_empty _ _ true with "Hs Hbox") as (Pb') "[EQ Hbox]".
+        solve_ndisj. by rewrite lookup_fmap EQB.
+      iDestruct (add_vs with "EQ Hvs HvsQ") as "Hvs".
+      iMod (slice_insert_empty _ _ true with "Hbox") as (j) "(% & #Hs' & Hbox)".
+      iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
+      { apply auth_update. etrans.
+        - apply delete_singleton_local_update, _.
+        - apply (alloc_singleton_local_update _ j
+                   (1%Qp, DecAgree (Bor_open q'))); last done.
+          rewrite -fmap_delete lookup_fmap fmap_None
+                  -fmap_None -lookup_fmap fmap_delete //. }
+      rewrite own_bor_op. iDestruct "Hown" as "[Hown Hbor]".
+      iMod (bor_close_internal _ _ (_, _) with "Hs' [Hbox Hown HB] Hbor HQ")
+        as "(Halive & Hbor & Htok)". solve_ndisj.
+      { rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ (Bor_open q'))
+                /lft_bor_alive. iExists _. iFrame "Hbox Hown".
+        rewrite big_sepM_insert. by rewrite big_sepM_delete.
+        by rewrite -fmap_None -lookup_fmap fmap_delete. }
+      iMod ("Hclose'" with "[-Hbor Htok Hclose]") as "_".
+      { iExists _, _. iFrame. rewrite big_sepS_later /lft_bor_alive. iApply "Hclose''".
+        iLeft. iFrame "%". iExists _, _. iFrame. }
+      iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
+      iSplit; first by iApply lft_incl_refl. iExists j. iFrame "∗#".
+    + 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 "[]".
+Qed.
+
+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) ∨
+    ([†κ] ∗ |={E∖↑lftN,E}=> True).
+Proof.
+  iIntros (HE) "#LFT Hbor". rewrite bor_unfold_idx /idx_bor /bor /raw_bor.
+  iDestruct "Hbor" as (i) "((#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. iExists (i.1). iFrame "#".
+    iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
+    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 (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "($ & EQ & Hbox)".
+      solve_ndisj. by rewrite lookup_fmap EQB.
+    iMod fupd_intro_mask' as "Hclose"; last iIntros "!>*HQ HvsQ". solve_ndisj.
+    iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs HvsQ") as "Hvs".
+    iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
+      solve_ndisj.
+    iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
+    { apply auth_update. etrans.
+      - apply delete_singleton_local_update, _.
+      - apply (alloc_singleton_local_update _ j (1%Qp, DecAgree (Bor_in))); last done.
+        rewrite -fmap_delete lookup_fmap fmap_None
+                -fmap_None -lookup_fmap fmap_delete //. }
+    rewrite own_bor_op. iDestruct "Hown" as "[H● H◯]".
+    iMod ("Hclose'" with "[- H◯]"); last first.
+    { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl.
+      iExists j. iFrame. done. }
+    iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
+    iLeft. iFrame "%". iExists _, _. iFrame. iNext.
+    rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in).
+    iExists _. iFrame "Hbox H●".
+    rewrite big_sepM_insert. by rewrite big_sepM_delete.
+      by rewrite -fmap_None -lookup_fmap fmap_delete.
+  - 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†") as "$". done.
+      iApply fupd_intro_mask'. solve_ndisj.
+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_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
+  iIntros "!>HP". iMod ("Hclose" with "*HP []") as "[Hb $]". by iIntros "!> $ _".
+  iApply (bor_shorten with "Hκκ' Hb").
+Qed.
+
+Lemma bor_acc_atomic E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
+       (▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ &{κ}P)) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True).
+Proof.
+  iIntros (?) "#LFT HP".
+  iMod (bor_acc_atomic_strong with "LFT HP") as "[H|[H† Hclose]]". done.
+  - iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>HP".
+    iApply (bor_shorten with "Hκκ'"). iApply ("Hclose" with "* HP []"). auto.
+  - iRight. by iFrame.
+Qed.
+End accessors.
\ No newline at end of file
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..c4e5f040eb40bf8da48a19b218d4feee5cbc2240
--- /dev/null
+++ b/theories/lifetime/borrow.v
@@ -0,0 +1,240 @@
+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.
+From iris.proofmode Require Import tactics.
+
+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)".
+  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. }
+  rewrite {1}/lft_inv. iDestruct "Hinv" as "[[Hinv >%]|[Hinv >%]]".
+  - 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 (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".
+    { eapply auth_update_alloc,
+        (alloc_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]").
+    { 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. }
+    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κ.
+      iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose']".
+      { by apply elem_of_dom. }
+      rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
+      iDestruct (own_alft_auth_agree A Λ false with "HA H†") as %EQAΛ.
+      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. }
+      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.
+    unfold bor. iExists κ. iFrame. rewrite -lft_incl_refl -big_sepS_later.
+    iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iNext.
+    rewrite /lft_inv. iRight. rewrite /lft_inv_dead. iFrame. eauto.
+Qed.
+
+Lemma bor_sep E κ P Q :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
+Proof.
+  iIntros (HE) "#Hmgmt HP". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  rewrite {1}/bor /raw_bor /idx_bor_own.
+  iDestruct "HP" as (κ') "[#Hκκ' Htmp]". iDestruct "Htmp" as (s) "[Hbor Hslice]".
+  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. simpl.
+  iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose']".
+  - rewrite lft_inv_alive_unfold /lft_bor_alive.
+    iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
+    iDestruct "H" as (B) "(Hbox & >Hown & HB)".
+    iDestruct (own_bor_valid_2 with "Hown Hbor")
+        as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+    iMod (slice_split _ _ true with "Hslice Hbox")
+      as (γ1 γ2) "(% & % & % & Hs1 & Hs2 & Hbox)"; first solve_ndisj.
+    { by rewrite lookup_fmap EQB. }
+    iMod (own_bor_update_2 with "Hown Hbor") as "Hbor".
+    { etrans; last etrans.
+      - apply auth_update_dealloc. by apply delete_singleton_local_update, _.
+      - apply auth_update_alloc,
+           (alloc_singleton_local_update _ γ1 (1%Qp, DecAgree Bor_in)); last done.
+        rewrite /to_borUR -fmap_delete lookup_fmap fmap_None
+                -fmap_None -lookup_fmap fmap_delete //.
+      - apply cmra_update_op; last done.
+        apply auth_update_alloc,
+          (alloc_singleton_local_update _ γ2 (1%Qp, DecAgree Bor_in)); last done.
+        rewrite lookup_insert_ne // /to_borUR -fmap_delete lookup_fmap fmap_None
+                -fmap_None -lookup_fmap fmap_delete //. }
+    rewrite !own_bor_op. iDestruct "Hbor" as "[[H● H◯2] H◯1]".
+    iAssert (&{κ}P)%I with "[H◯1 Hs1]" as "$".
+    { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1. iFrame. }
+    iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
+    { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2. iFrame. }
+    iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
+    iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
+    rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
+    rewrite !big_sepM_insert /=.
+    + by rewrite left_id -(big_sepM_delete _ _ _ _ EQB).
+    + by rewrite -fmap_None -lookup_fmap fmap_delete.
+    + by rewrite lookup_insert_ne // -fmap_None -lookup_fmap fmap_delete.
+  - iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
+    iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor1]"; first solve_ndisj.
+    iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor2]"; first solve_ndisj.
+    iMod ("Hclose" with "[-Hbor1 Hbor2]") as "_".
+    { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
+      iRight. iSplit; last by auto. iExists _. iFrame. }
+    unfold bor. iSplitL "Hbor1"; iExists _; eauto.
+Qed.
+
+Lemma bor_combine E κ P Q :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
+Proof.
+  iIntros (?) "#Hmgmt HP HQ". rewrite {1 2}/bor.
+  iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
+  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor1") as "[Hbor1 _]".
+    done. by apply gmultiset_union_subseteq_l.
+  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor2") as "[Hbor2 _]".
+    done. by apply gmultiset_union_subseteq_r.
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
+  iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
+  iDestruct (own_bor_auth with "HI Hbor1") as %Hκ'.
+  rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
+          /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in. simpl.
+  iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose']".
+  - rewrite lft_inv_alive_unfold /lft_bor_alive.
+    iDestruct "Hinv" as (Pb Pi) "(H & Hvs & Hinh)".
+    iDestruct "H" as (B) "(Hbox & >Hown & HB)".
+    iDestruct (own_bor_valid_2 with "Hown Hbor1")
+        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.
+    { iIntros (->).
+      iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
+      exfalso. revert Hj1j2. rewrite /= op_singleton singleton_valid.
+      compute. tauto. }
+    iMod (slice_combine _ _ true with "Hslice1 Hslice2 Hbox")
+      as (γ) "(% & Hslice & Hbox)"; first solve_ndisj.
+    { done. }
+    { by rewrite lookup_fmap EQB1. }
+    { by rewrite lookup_fmap EQB2. }
+    iCombine "Hown" "Hbor1" as "Hbor1". iCombine "Hbor1" "Hbor2" as "Hbor".
+    rewrite -!own_bor_op. iMod (own_bor_update with "Hbor") as "Hbor".
+    { etrans; last etrans.
+      - apply cmra_update_op; last done.
+        apply auth_update_dealloc. by apply delete_singleton_local_update, _.
+      - apply auth_update_dealloc. by apply delete_singleton_local_update, _.
+      - apply auth_update_alloc,
+           (alloc_singleton_local_update _ γ (1%Qp, DecAgree Bor_in)); last done.
+        rewrite /to_borUR -!fmap_delete lookup_fmap fmap_None
+                -fmap_None -lookup_fmap !fmap_delete //. }
+    rewrite own_bor_op. iDestruct "Hbor" as "[H● H◯]".
+    iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
+    { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2). 
+      iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
+      iExists γ. iFrame. } 
+    iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
+    iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
+    rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
+    rewrite !big_sepM_insert /=.
+    + rewrite (big_sepM_delete _ _ _ _ EQB1) /=.
+      rewrite (big_sepM_delete _ _ j2 Bor_in) /=. by iDestruct "HB" as "[_ $]".
+      rewrite lookup_delete_ne //.
+    + rewrite -fmap_None -lookup_fmap !fmap_delete //.
+  - iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
+    iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
+    iMod ("Hclose" with "[-Hbor]") as "_".
+    { iExists A, I. iFrame. rewrite big_sepS_later. iApply "Hclose'".
+      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/creation.v
new file mode 100644
index 0000000000000000000000000000000000000000..9dd4c7becc3e12c583f2b97f90fb9254270eb423
--- /dev/null
+++ b/theories/lifetime/creation.v
@@ -0,0 +1,294 @@
+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 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 κ') -∗
+    ([∗ set] κ' ∈ KI, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ') ∗
+    (([∗ set] κ' ∈ KI, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ') -∗
+      ([∗ set] κ' ∈ K, lft_inv_alive κ')).
+Proof.
+  intros ?.
+  destruct (proj1 (subseteq_disjoint_union_L (filter (⊂ κ) KI) K)) as (K'&->&?).
+  { intros κ'. rewrite elem_of_filter. set_solver. }
+  rewrite big_sepS_union // big_sepS_filter. iIntros "[$ $]"; auto.
+Qed.
+
+Lemma ilft_create A I κ :
+  own_ilft_auth I -∗ own_alft_auth A -∗ ▷ ([∗ 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' κ).
+Proof.
+  iIntros "HI HA HA'".
+  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.
+  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 (lft_inv_dead κ ∧ lft_inv_alive κ)%I
+    with "[-HA HA' HI]" 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_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. }
+  destruct (lft_alive_or_dead_in A κ) as [(Λ&?&HAΛ)|Haliveordead].
+  - iMod (own_update with "HA") as "[HA _]".
+    { apply auth_update_alloc,
+        (alloc_singleton_local_update _ Λ (Cinr ())); last done.
+      by rewrite lookup_fmap HAΛ. }
+    iModIntro. iExists (<[Λ:=false]>A), (<[κ:=γs]> I).
+    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'".
+    { rewrite /lft_inv. iNext. iRight. iSplit.
+      { by iDestruct "Hdeadandalive" as "[? _]". }
+      iPureIntro. exists Λ. rewrite lookup_insert; auto. }
+    iNext. iApply (@big_sepS_impl with "[$HA']").
+    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.
+    + iLeft. by iDestruct "Hdeadandalive" as "[_ $]".
+    + iRight. by iDestruct "Hdeadandalive" as "[$ _]".
+Qed.
+
+Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
+  let Iinv := (
+    own_ilft_auth I ∗
+    ([∗ set] κ' ∈ K, lft_inv_alive κ') ∗
+    ([∗ set] κ' ∈ K', lft_inv_dead κ'))%I in
+  (∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K) →
+  (∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K') →
+  Iinv -∗ lft_inv_alive κ -∗ [†κ] ={⊤∖↑mgmtN}=∗ Iinv ∗ lft_inv_dead κ.
+Proof.
+  iIntros (Iinv HK HK') "(HI & Halive & Hdead) Hlalive Hκ".
+  rewrite lft_inv_alive_unfold;
+    iDestruct "Hlalive" as (P Q) "(Hbor & Hvs & Hinh)".
+  rewrite /lft_bor_alive; iDestruct "Hbor" as (B) "(Hbox & Hbor & HB)".
+  iAssert ⌜∀ i s, B !! i = Some s → s = Bor_in⌝%I with "[#]" as %HB.
+  { iIntros (i s HBI).
+    iDestruct (big_sepM_lookup _ B with "HB") as "HB"=> //.
+    destruct s as [|q|κ']; rewrite /bor_cnt //.
+    { iDestruct (lft_tok_dead with "HB Hκ") as "[]". }
+    iDestruct "HB" as "[% Hcnt]".
+    iDestruct (own_cnt_auth with "HI Hcnt") as %?.
+    iDestruct (@big_sepS_elem_of with "Hdead") as "Hdead"; first by eauto.
+    rewrite /lft_inv_dead; iDestruct "Hdead" as (R) "(_ & Hcnt' & _)".
+    iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
+      as %[?%nat_included _]%auth_valid_discrete_2; omega. }
+  iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first solve_ndisj.
+  { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
+  rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
+  iDestruct (lft_inv_alive_acc (dom _ I) _ κ with "Halive") as "[Halive Halive']".
+  { intros κ'. rewrite elem_of_dom. eauto. }
+  iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
+  { rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
+    iExists (dom _ B), P. rewrite !to_gmap_dom -map_fmap_compose.
+    rewrite (map_fmap_ext _ ((1%Qp,) ∘ DecAgree) B); last naive_solver.
+    iFrame. }
+  rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(?&HI&Halive)".
+  iSpecialize ("Halive'" with "Halive").
+  iMod (own_cnt_update_2 with "Hcnt Hcnt'") as "?".
+  { apply auth_update_dealloc, (nat_local_update _ _ 0 0); omega. }
+  rewrite /Iinv. iFrame "Hdead Halive' HI".
+  iMod (lft_inh_kill with "[$Hinh $HQ]"); first solve_ndisj.
+  iModIntro. rewrite /lft_inv_dead. iExists Q. by iFrame.
+Qed.
+
+Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) :
+  let Iinv K' := (own_ilft_auth I ∗ [∗ set] κ' ∈ K', lft_inv_alive κ')%I in
+  (∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →
+  (∀ κ κ', κ ∈ K → lft_alive_in A κ → is_Some (I !! κ') →
+    κ' ∉ K → κ' ⊂ κ → κ' ∈ K') →
+  Iinv K' -∗ ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])
+    ={⊤∖↑mgmtN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
+Proof.
+  intros Iinv. revert K'.
+  induction (collection_wf K) as [K _ IH]=> K' HK HK'.
+  iIntros "[HI Halive] HK".
+  pose (Kalive := filter (lft_alive_in A) K).
+  destruct (decide (Kalive = ∅)) as [HKalive|].
+  { iModIntro. rewrite /Iinv. iFrame.
+    iApply (@big_sepS_impl with "[$HK]"); iAlways.
+    rewrite /lft_inv. iIntros (κ Hκ) "[[[_ %]|[$ _]] _]". set_solver. }
+  destruct (minimal_exists_L (⊂) Kalive)
+    as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
+  iDestruct (@big_sepS_delete with "HK") as "[[Hκinv Hκ] HK]"; first done.
+  iDestruct (lft_inv_alive_in with "Hκinv") as "Hκalive"; first done.
+  iAssert ⌜κ ∉ K'⌝%I with "[#]" as %HκK'.
+  { iIntros (Hκ). iApply (lft_inv_alive_twice κ with "Hκalive").
+    by iApply (@big_sepS_elem_of with "Halive"). }
+  specialize (IH (K ∖ {[ κ ]})). feed specialize IH; [set_solver +HκK|].
+  iMod (IH ({[ κ ]} ∪ K') with "[HI Halive Hκalive] HK") as "[[HI Halive] Hdead]".
+  { intros κ' κ''.
+    rewrite !elem_of_difference !elem_of_singleton=> -[? Hneq] ??.
+    split; [by eauto|]; intros ->.
+    eapply (minimal_strict_1 _ _ κ' Hκmin), strict_spec_alt; eauto.
+    apply elem_of_filter; eauto using lft_alive_in_subseteq. }
+  { intros κ' κ'' Hκ' ? [γs'' ?].
+    destruct (decide (κ'' = κ)) as [->|]; [set_solver +|].
+    move: Hκ'; rewrite not_elem_of_difference elem_of_difference
+       elem_of_union not_elem_of_singleton elem_of_singleton.
+    intros [??] [?|?]; eauto. }
+  { rewrite /Iinv big_sepS_insert //. iFrame. }
+  iDestruct (@big_sepS_insert with "Halive") as "[Hκalive Halive]"; first done.
+  iMod (lft_kill with "[$HI $Halive $Hdead] Hκalive Hκ")
+    as "[(HI&Halive&Hdead) Hκdead]".
+  { intros κ' ??. eapply (HK' κ); eauto.
+    intros ?. eapply (minimal_strict_1 _ _ _ Hκmin); eauto.
+    apply elem_of_filter; split; last done.
+    eapply lft_alive_in_subseteq, gmultiset_subset_subseteq; eauto. }
+  { intros κ' ? [??]%strict_spec_alt.
+    rewrite elem_of_difference elem_of_singleton; eauto. }
+  iModIntro. rewrite /Iinv (big_sepS_delete _ K) //. iFrame.
+Qed.
+
+Definition kill_set (I : gmap lft lft_names) (Λ : atomic_lft) : gset lft :=
+  filter (Λ ∈) (dom (gset lft) I).
+
+Lemma elem_of_kill_set I Λ κ : κ ∈ kill_set I Λ ↔ Λ ∈ κ ∧ is_Some (I !! κ).
+Proof. by rewrite /kill_set elem_of_filter elem_of_dom. Qed.
+Lemma kill_set_subseteq I Λ : kill_set I Λ ⊆ dom (gset lft) I.
+Proof. intros κ [??]%elem_of_kill_set. by apply elem_of_dom. Qed.
+
+Definition down_close (A : gmap atomic_lft bool)
+    (I : gmap lft lft_names) (K : gset lft) : gset lft :=
+  filter (λ κ, κ ∉ K ∧
+    set_Exists (λ κ', κ ⊂ κ' ∧ lft_alive_in A κ') K) (dom (gset lft) I).
+Lemma elem_of_down_close A I K κ :
+  κ ∈ down_close A I K ↔
+    is_Some (I !! κ) ∧ κ ∉ K ∧ ∃ κ', κ' ∈ K ∧ κ ⊂ κ' ∧ lft_alive_in A κ'.
+Proof. rewrite /down_close elem_of_filter elem_of_dom /set_Exists. tauto. Qed.
+
+Lemma down_close_lft_alive_in A I K κ : κ ∈ down_close A I K → lft_alive_in A κ.
+Proof.
+  rewrite elem_of_down_close; intros (?&?&?&?&?&?).
+  eapply lft_alive_in_subseteq, gmultiset_subset_subseteq; eauto.
+Qed.
+Lemma down_close_disjoint A I K : K ⊥ down_close A I K.
+Proof. intros κ. rewrite elem_of_down_close. naive_solver. Qed.
+Lemma down_close_subseteq A I K :
+  down_close A I K ⊆ dom (gset lft) I.
+Proof. intros κ [??]%elem_of_down_close. by apply elem_of_dom. Qed.
+
+Lemma lft_create E :
+  ↑lftN ⊆ E →
+  lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
+Proof.
+  iIntros (?) "#Hmgmt".
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  destruct (exist_fresh (dom (gset _) A)) as [Λ HΛ%not_elem_of_dom].
+  iMod (own_update with "HA") as "[HA HΛ]".
+  { apply auth_update_alloc, (alloc_singleton_local_update _ Λ (Cinl 1%Qp))=>//.
+    by rewrite lookup_fmap HΛ. }
+  iMod ("Hclose" with "[HA HI Hinv]") as "_".
+  { iNext. rewrite /lfts_inv /own_alft_auth.
+    iExists (<[Λ:=true]>A), I. rewrite /to_alftUR fmap_insert; iFrame.
+    iApply (@big_sepS_impl with "[$Hinv]").
+    iAlways. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
+    - iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
+    - iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
+  iModIntro; iExists {[ Λ ]}.
+  rewrite {1}/lft_tok big_sepMS_singleton. iFrame "HΛ".
+  clear I A HΛ. iIntros "!# HΛ".
+  iApply (step_fupd_mask_mono ⊤ _ _ (⊤∖↑mgmtN)); [solve_ndisj..|].
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  rewrite /lft_tok big_sepMS_singleton.
+  iDestruct (own_valid_2 with "HA HΛ")
+    as %[[s [?%leibniz_equiv ?]]%singleton_included _]%auth_valid_discrete_2.
+  iMod (own_update_2 with "HA HΛ") as "[HA HΛ]".
+  { by eapply auth_update, singleton_local_update,
+      (exclusive_local_update _ (Cinr ())). }
+  iDestruct "HΛ" as "#HΛ". iModIntro; iNext.
+  pose (K := kill_set I Λ); pose (K' := down_close A I K).
+  assert (K ⊥ K') by (by apply down_close_disjoint).
+  destruct (proj1 (subseteq_disjoint_union_L (K ∪ K')
+    (dom (gset lft) I))) as (K''&HI&?).
+  { apply union_least. apply kill_set_subseteq. apply down_close_subseteq. }
+  rewrite HI !big_sepS_union //. iDestruct "Hinv" as "[[HinvK HinvD] Hinv]".
+  iAssert ([∗ set] κ ∈ K', lft_inv_alive κ)%I with "[HinvD]" as "HinvD".
+  { iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
+    iIntros (κ Hκ) "?". iApply lft_inv_alive_in; last done.
+    eauto using down_close_lft_alive_in. }
+  iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [† κ])%I with "[HinvK]" as "HinvK". 
+  { iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
+    iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
+  iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
+  { intros κ κ' [??]%elem_of_kill_set ??. apply elem_of_kill_set.
+    split; last done. by eapply gmultiset_elem_of_subseteq. }
+  { intros κ κ' ?????. apply elem_of_down_close; eauto 10. }
+  iMod ("Hclose" with "[-]") as "_"; last first.
+  { iModIntro. rewrite /lft_dead. iExists Λ.
+    rewrite elem_of_singleton. auto. }
+  iNext. iExists (<[Λ:=false]>A), I.
+  rewrite /own_alft_auth /to_alftUR fmap_insert. iFrame "HA HI".
+  rewrite HI !big_sepS_union //.
+  iSplitL "HinvK HinvD"; first iSplitL "HinvK".
+  - iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
+    iIntros (κ [? _]%elem_of_kill_set) "Hdead". rewrite /lft_inv.
+    iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false'.
+  - iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
+    iIntros (κ Hκ) "Halive". rewrite /lft_inv.
+    iLeft. iFrame "Halive". iPureIntro.
+    assert (lft_alive_in A κ) as Halive by (by eapply down_close_lft_alive_in).
+    apply lft_alive_in_insert_false; last done.
+    apply elem_of_down_close in Hκ as (?&HFOO&_).
+    move: HFOO. rewrite elem_of_kill_set. tauto.
+  - iApply (@big_sepS_impl with "[$Hinv]"); iIntros "!#".
+    rewrite /lft_inv. iIntros (κ Hκ) "[[? %]|[? %]]".
+    + iLeft. iFrame. iPureIntro.
+      apply lft_alive_in_insert_false; last done.
+      assert (κ ∉ K). intros ?. eapply H5. 2: eauto. rewrite elem_of_union. eauto.
+      move: H7. rewrite elem_of_kill_set not_and_l. intros [?|?]. done.
+contradict H7. apply elem_of_dom. set_solver +HI Hκ.
+    + iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false.
+Qed.
+End creation.
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
new file mode 100644
index 0000000000000000000000000000000000000000..995a2fb3d3f0439feb92902d31792376b2eaf8d6
--- /dev/null
+++ b/theories/lifetime/definitions.v
@@ -0,0 +1,307 @@
+From iris.algebra Require Import csum auth frac gmap dec_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.base_logic Require Import big_op.
+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.
+
+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.
+
+Definition alftUR := gmapUR atomic_lft lft_stateR.
+Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
+
+Definition ilftUR := gmapUR lft (dec_agreeR lft_names).
+Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap DecAgree.
+
+Definition borUR := gmapUR slice_name (prodR fracR (dec_agreeR bor_state)).
+Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ DecAgree).
+
+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_box :> inG Σ (authR borUR);
+  lft_cnt_inG :> inG Σ (authR natUR);
+  lft_inh_box :> inG Σ (authR inhUR);
+}.
+
+Section defs.
+  Context `{invG Σ, lftG Σ}.
+
+  Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
+    ([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
+
+  Definition lft_dead (κ : lft) : iProp Σ :=
+    (∃ Λ, ⌜Λ ∈ κ⌝ ∗ own alft_name (◯ {[ Λ := Cinr () ]}))%I.
+
+  Definition own_alft_auth (A : gmap atomic_lft bool) : iProp Σ :=
+    own alft_name (● to_alftUR A).
+  Definition own_ilft_auth (I : gmap lft lft_names) : iProp Σ :=
+    own ilft_name (● to_ilftUR I).
+
+  Definition own_bor (κ : lft)
+      (x : auth (gmap slice_name (frac * dec_agree bor_state))) : iProp Σ :=
+    (∃ γs,
+      own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
+      own (bor_name γs) x)%I.
+
+  Definition own_cnt (κ : lft) (x : auth nat) : iProp Σ :=
+    (∃ γs,
+      own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
+      own (cnt_name γs) x)%I.
+
+  Definition own_inh (κ : lft) (x : auth (gset_disj slice_name)) : iProp Σ :=
+    (∃ γs,
+      own ilft_name (◯ {[ κ := DecAgree γs ]}) ∗
+      own (inh_name γs) x)%I.
+
+  Definition bor_cnt (κ : lft) (s : bor_state) : iProp Σ :=
+    match s with
+    | Bor_in => True
+    | Bor_open q => lft_tok q κ
+    | Bor_rebor κ' => ⌜κ ⊂ κ'⌝ ∗ own_cnt κ' (◯ 1)
+    end%I.
+
+  Definition lft_bor_alive (κ : lft) (Pi : iProp Σ) : iProp Σ :=
+    (∃ B : gmap slice_name bor_state,
+      box borN (bor_filled <$> B) Pi ∗
+      own_bor κ (● to_borUR B) ∗
+      [∗ map] s ∈ B, bor_cnt κ s)%I.
+
+  Definition lft_bor_dead (κ : lft) : iProp Σ :=
+     (∃ (B: gset slice_name) (Pb : iProp Σ),
+       own_bor κ (● to_gmap (1%Qp, DecAgree Bor_in) B) ∗
+       box borN (to_gmap false B) Pb)%I.
+
+   Definition lft_inh (κ : lft) (s : bool) (Pi : iProp Σ) : iProp Σ :=
+     (∃ E : gset slice_name,
+       own_inh κ (● GSet E) ∗
+       box inhN (to_gmap s E) Pi)%I.
+
+   Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
+       (I : gmap lft lft_names) : iProp Σ :=
+     (lft_bor_dead κ ∗
+       own_ilft_auth I ∗
+       [∗ set] κ' ∈ dom _ I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ)%I.
+
+   Definition lft_vs_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
+       (Pb Pi : iProp Σ) : iProp Σ :=
+     (∃ n : nat,
+       own_cnt κ (● n) ∗
+       ∀ I : gmap lft lft_names,
+         lft_vs_inv_go κ lft_inv_alive I -∗ ▷ Pb -∗ lft_dead κ
+           ={⊤∖↑mgmtN}=∗
+         lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Pi ∗ own_cnt κ (◯ n))%I.
+
+  Definition lft_inv_alive_go (κ : lft)
+      (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ) : iProp Σ :=
+    (∃ Pb Pi,
+      lft_bor_alive κ Pb ∗
+      lft_vs_go κ lft_inv_alive Pb Pi ∗
+      lft_inh κ false Pi)%I.
+
+  Definition lft_inv_alive (κ : lft) : iProp Σ :=
+    Fix_F _ lft_inv_alive_go (gmultiset_wf κ).
+  Definition lft_vs_inv (κ : lft) (I : gmap lft lft_names) : iProp Σ :=
+    lft_vs_inv_go κ (λ κ' _, lft_inv_alive κ') I.
+  Definition lft_vs (κ : lft) (Pb Pi : iProp Σ) : iProp Σ :=
+    lft_vs_go κ (λ κ' _, lft_inv_alive κ') Pb Pi.
+
+  Definition lft_inv_dead (κ : lft) : iProp Σ :=
+    (∃ Pi,
+      lft_bor_dead κ ∗
+      own_cnt κ (● 0) ∗
+      lft_inh κ true Pi)%I.
+
+  Definition lft_alive_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
+    ∀ Λ : atomic_lft, Λ ∈ κ → A !! Λ = Some true.
+  Definition lft_dead_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
+    ∃ Λ : atomic_lft, Λ ∈ κ ∧ A !! Λ = Some false.
+
+  Definition lft_inv (A : gmap atomic_lft bool) (κ : lft) : iProp Σ :=
+    (lft_inv_alive κ ∗ ⌜lft_alive_in A κ⌝ ∨
+     lft_inv_dead κ ∗ ⌜lft_dead_in A κ⌝)%I.
+
+  Definition lfts_inv : iProp Σ :=
+    (∃ (A : gmap atomic_lft bool) (I : gmap lft lft_names),
+      own_alft_auth A ∗
+      own_ilft_auth I ∗
+      [∗ set] κ ∈ dom _ I, lft_inv A κ)%I.
+
+  Definition lft_ctx : iProp Σ := inv mgmtN lfts_inv.
+
+  Definition lft_incl (κ κ' : lft) : iProp Σ :=
+    (□ ((∀ q, lft_tok q κ ={↑lftN}=∗ ∃ q',
+                 lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
+        (lft_dead κ' ={↑lftN}=∗ lft_dead κ)))%I.
+
+  Definition bor_idx := (lft * slice_name)%type.
+
+  Definition idx_bor_own (q : frac) (i : bor_idx) : iProp Σ :=
+    own_bor (i.1) (◯ {[ i.2 := (q,DecAgree Bor_in) ]}).
+  Definition idx_bor (κ : lft) (i : bor_idx) (P : iProp Σ) : iProp Σ :=
+    (lft_incl κ (i.1) ∗ slice borN (i.2) P)%I.
+  Definition raw_bor (κ : lft) (P : iProp Σ) : iProp Σ :=
+    (∃ s : slice_name, idx_bor_own 1 (κ, s) ∗ slice borN s P)%I.
+  Definition bor (κ : lft) (P : iProp Σ) : iProp Σ :=
+    (∃ κ', lft_incl κ κ' ∗ raw_bor κ' P)%I.
+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.
+
+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.
+
+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.
+
+Section basic_properties.
+Context `{invG Σ, lftG Σ}.
+Implicit Types κ : lft.
+
+(* Unfolding lemmas *)
+Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) I n :
+  (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
+  lft_vs_inv_go κ f I ≡{n}≡ lft_vs_inv_go κ f' I.
+Proof.
+  intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ'.
+  by apply forall_ne=> Hκ.
+Qed.
+
+Lemma lft_vs_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) Pb Pb' Pi Pi' n :
+  (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
+  Pb ≡{n}≡ Pb' → Pi ≡{n}≡ Pi' →
+  lft_vs_go κ f Pb Pi ≡{n}≡ lft_vs_go κ f' Pb' Pi'.
+Proof.
+  intros Hf HPb HPi. apply exist_ne=> n'.
+  apply sep_ne, forall_ne=> // I. rewrite lft_vs_inv_go_ne //. solve_proper.
+Qed.
+
+Lemma lft_inv_alive_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) n :
+  (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
+  lft_inv_alive_go κ f ≡{n}≡ lft_inv_alive_go κ f'.
+Proof.
+  intros Hf. apply exist_ne=> Pb; apply exist_ne=> Pi. by rewrite lft_vs_go_ne.
+Qed.
+
+Lemma lft_inv_alive_unfold κ :
+  lft_inv_alive κ ⊣⊢ ∃ Pb Pi,
+    lft_bor_alive κ Pb ∗ lft_vs κ Pb Pi ∗ lft_inh κ false Pi.
+Proof.
+  apply equiv_dist=> n. rewrite /lft_inv_alive -Fix_F_eq.
+  apply lft_inv_alive_go_ne=> κ' Hκ.
+  apply (Fix_F_proper _ (λ _, dist n)); auto using lft_inv_alive_go_ne.
+Qed.
+Lemma lft_vs_inv_unfold κ (I : gmap lft lft_names) :
+  lft_vs_inv κ I ⊣⊢ lft_bor_dead κ ∗
+    own_ilft_auth I ∗
+    [∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ'.
+Proof.
+  rewrite /lft_vs_inv /lft_vs_inv_go. by setoid_rewrite pure_impl_forall.
+Qed.
+Lemma lft_vs_unfold κ Pb Pi :
+  lft_vs κ Pb Pi ⊣⊢ ∃ n : nat,
+    own_cnt κ (● n) ∗
+    ∀ I : gmap lft lft_names,
+      lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={⊤∖↑mgmtN}=∗
+      lft_vs_inv κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n).
+Proof. done. Qed.
+
+Global Instance lft_bor_alive_ne κ n : Proper (dist n ==> dist n) (lft_bor_alive κ).
+Proof. solve_proper. Qed.
+Global Instance lft_bor_alive_proper κ : Proper ((≡) ==> (≡)) (lft_bor_alive κ).
+Proof. apply (ne_proper _). Qed.
+
+Global Instance lft_inh_ne κ s n : Proper (dist n ==> dist n) (lft_inh κ s).
+Proof. solve_proper. Qed.
+Global Instance lft_inh_proper κ s : Proper ((≡) ==> (≡)) (lft_inh κ s).
+Proof. apply (ne_proper _). Qed.
+
+Global Instance lft_vs_ne κ n :
+  Proper (dist n ==> dist n ==> dist n) (lft_vs κ).
+Proof. intros P P' HP Q Q' HQ. by apply lft_vs_go_ne. Qed.
+Global Instance lft_vs_proper κ : Proper ((≡) ==> (≡) ==> (≡)) (lft_vs κ).
+Proof. apply (ne_proper_2 _). Qed.
+
+Global Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
+Proof. solve_proper. Qed.
+Global Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
+Proof. apply (ne_proper _). Qed.
+
+Global Instance raw_bor_ne i n : Proper (dist n ==> dist n) (raw_bor i).
+Proof. solve_proper. Qed.
+Global Instance raw_bor_proper i : Proper ((≡) ==> (≡)) (raw_bor i).
+Proof. apply (ne_proper _). Qed.
+
+Global Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
+Proof. solve_proper. Qed.
+Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
+Proof. apply (ne_proper _). Qed.
+
+(*** PersistentP and TimelessP and instances  *)
+Global Instance lft_tok_timeless q κ : TimelessP q.[κ].
+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_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
+Proof. rewrite /lft_incl. apply _. Qed.
+
+Global Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
+Proof. rewrite /idx_bor. apply _. Qed.
+Global Instance idx_bor_own_timeless q i : TimelessP (idx_bor_own q i).
+Proof. rewrite /idx_bor_own. apply _. Qed.
+
+Global Instance lft_ctx_persistent : PersistentP lft_ctx.
+Proof. rewrite /lft_ctx. apply _. Qed.
+End basic_properties.
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
new file mode 100644
index 0000000000000000000000000000000000000000..917552ef38724b7237a3003b9518846166e89960
--- /dev/null
+++ b/theories/lifetime/derived.v
@@ -0,0 +1,65 @@
+From lrust.lifetime Require Export primitive borrow accessors rebor.
+From iris.proofmode Require Import tactics.
+
+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").
+Qed.
+
+Lemma bor_or E κ P Q :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
+Proof.
+  iIntros (?) "#LFT H". rewrite uPred.or_alt.
+  iMod (bor_exists with "LFT H") as ([]) "H"; auto.
+Qed.
+
+Lemma bor_later E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ}(▷ P) ={E,E∖↑lftN}▷=∗ &{κ}P.
+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").
+Qed.
+
+Lemma bor_later_tok E q κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].
+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 "!>$_".
+  by iApply (bor_shorten with "Hκκ'").
+Qed.
+
+Lemma bor_persistent P `{!PersistentP P} E κ q :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
+Proof.
+  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.
+Proof.
+  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/frac_borrow.v b/theories/lifetime/frac_borrow.v
similarity index 69%
rename from theories/frac_borrow.v
rename to theories/lifetime/frac_borrow.v
index 64f595dd8a222f28043d677142a05060dc638249..c390bfcef9d7bd20db71f4268380e4a2ac4a7bcc 100644
--- a/theories/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -2,64 +2,64 @@ 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 Require Export lifetime shr_borrow.
+From lrust.lifetime Require Export shr_borrow .
 
-Class frac_borrowG Σ := frac_borrowG_inG :> inG Σ fracR.
+Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Definition frac_borrow `{invG Σ, lifetimeG Σ, frac_borrowG Σ} κ (Φ : Qp → iProp Σ) :=
+Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (Φ : Qp → iProp Σ) :=
   (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
                        (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
-Notation "&frac{ κ } P" := (frac_borrow κ P)
+Notation "&frac{ κ } P" := (frac_bor κ P)
   (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
 
-Section frac_borrow.
-  Context `{invG Σ, lifetimeG Σ, frac_borrowG Σ}.
+Section frac_bor.
+  Context `{invG Σ, lftG Σ, frac_borG Σ}.
   Implicit Types E : coPset.
 
-  Global Instance frac_borrow_proper :
-    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_borrow κ).
+  Global Instance frac_bor_proper :
+    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_bor κ).
   Proof. solve_proper. Qed.
-  Global Instance frac_borrow_persistent : PersistentP (&frac{κ}Φ) := _.
+  Global Instance frac_bor_persistent : PersistentP (&frac{κ}Φ) := _.
 
-  Lemma borrow_fracture φ E κ :
+  Lemma bor_fracture φ E κ :
     ↑lftN ⊆ E → lft_ctx -∗ &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ.
   Proof.
     iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
-    iMod (borrow_acc_atomic_strong with "LFT Hφ") as "[[Hφ Hclose]|[H† Hclose]]". done.
-    - iMod ("Hclose" with "*[-]") as "Hφ"; last first.
-      { iExists γ, κ. iSplitR; last by iApply (borrow_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_own_dead with "Hκ H†") as "[]".
-    - iMod ("Hclose" with "*") as "HΦ"; last first.
+    iMod (bor_acc_atomic_strong with "LFT Hφ") as "[H|[H† Hclose]]". done.
+    - iDestruct "H" as (κ') "(#Hκκ' & Hφ & Hclose)".
+      iMod ("Hclose" with "*[-] []") as "Hφ"; last first.
+      { iExists γ, κ'. iFrame "#". iApply (bor_share with "Hφ"). done. }
+      { 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 "_"; last first.
       iExists γ, κ. iSplitR. by iApply lft_incl_refl.
-      iMod (borrow_fake with "LFT H†"). done. by iApply borrow_share.
+      iMod (bor_fake with "LFT H†"). done. by iApply bor_share.
   Qed.
 
-  Lemma frac_borrow_atomic_acc E κ φ :
+  Lemma frac_bor_atomic_acc E κ φ :
     ↑lftN ⊆ E →
     lft_ctx -∗ &frac{κ}φ ={E,E∖↑lftN}=∗ (∃ q, ▷ φ q ∗ (▷ φ q ={E∖↑lftN,E}=∗ True))
                                       ∨ [†κ] ∗ |={E∖↑lftN,E}=> True.
   Proof.
     iIntros (?) "#LFT #Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]".
-    iMod (shr_borrow_acc with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]". done.
+    iMod (shr_bor_acc with "LFT Hshr") as "[[Hφ Hclose]|[H† Hclose]]". done.
     - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
       iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
     - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
       iApply fupd_intro_mask. set_solver. done.
   Qed.
 
-  Lemma frac_borrow_acc_strong E q κ Φ:
+  Lemma frac_bor_acc_strong E q κ Φ:
     ↑lftN ⊆ E →
     lft_ctx -∗ □ (∀ q1 q2, Φ (q1+q2)%Qp ↔ Φ q1 ∗ Φ q2) -∗
     &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
   Proof.
-    iIntros (?) "#LFT #HΦ Hfrac Hκ". unfold frac_borrow.
+    iIntros (?) "#LFT #HΦ Hfrac Hκ". unfold frac_bor.
     iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
     iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done.
-    iMod (shr_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
+    iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
     iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & Hq)".
     destruct (Qp_lower_bound (qκ'/2) (qΦ/2)) as (qq & qκ'0 & qΦ0 & Hqκ' & HqΦ).
     iExists qq.
@@ -74,7 +74,7 @@ Section frac_borrow.
       - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp.
         iIntros "{$Hκq $Hq'κ}!%". by rewrite assoc (comm _ _ qq) assoc -HqΦ Qp_div_2. }
     clear HqΦ qΦ qΦ0. iIntros "!>HqΦ".
-    iMod (shr_borrow_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
+    iMod (shr_bor_acc_tok with "LFT Hshr Hκ1") as "[H Hclose']". done.
     iDestruct "H" as (qΦ) "(HΦqΦ & >Hown & >[%|Hq])".
     { subst. iCombine "Hown" "Hownq" as "Hown".
       by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. }
@@ -97,33 +97,33 @@ Section frac_borrow.
       iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
   Qed.
 
-  Lemma frac_borrow_acc E q κ `{Fractional _ Φ} :
+  Lemma frac_bor_acc E q κ `{Fractional _ Φ} :
     ↑lftN ⊆ E →
     lft_ctx -∗ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
   Proof.
-    iIntros (?) "LFT". iApply (frac_borrow_acc_strong with "LFT"). done.
+    iIntros (?) "LFT". iApply (frac_bor_acc_strong with "LFT"). done.
     iIntros "!#*". rewrite fractional. iSplit; auto.
   Qed.
 
-  Lemma frac_borrow_shorten κ κ' Φ: κ ⊑ κ' -∗ &frac{κ'}Φ -∗ &frac{κ}Φ.
+  Lemma frac_bor_shorten κ κ' Φ: κ ⊑ κ' -∗ &frac{κ'}Φ -∗ &frac{κ}Φ.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[#H⊑ ?]". iExists γ, κ0. iFrame.
     iApply (lft_incl_trans with "Hκκ' []"). auto.
   Qed.
 
-  Lemma frac_borrow_incl κ κ' q:
+  Lemma frac_bor_incl κ κ' q:
     lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
   Proof.
     iIntros "#LFT#Hbor!#". iSplitR.
     - iIntros (q') "Hκ'".
-      iMod (frac_borrow_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
+      iMod (frac_bor_acc with "LFT Hbor Hκ'") as (q'') "[>? Hclose]". done.
       iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto.
     - iIntros "H†'".
-      iMod (frac_borrow_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
+      iMod (frac_bor_atomic_acc with "LFT Hbor") as "[H|[$ $]]". done.
       iDestruct "H" as (q') "[>Hκ' _]".
-      iDestruct (lft_own_dead with "Hκ' H†'") as "[]".
+      iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
   Qed.
 
-End frac_borrow.
+End frac_bor.
 
-Typeclasses Opaque frac_borrow.
+Typeclasses Opaque frac_bor.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
new file mode 100644
index 0000000000000000000000000000000000000000..83ccf906a54bc3f19125efd8feed72795d6c932d
--- /dev/null
+++ b/theories/lifetime/primitive.v
@@ -0,0 +1,306 @@
+From lrust.lifetime Require Export definitions.
+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 fractional.
+From iris.proofmode Require Import tactics.
+Import uPred.
+
+Section primitive.
+Context `{invG Σ, lftG Σ}.
+Implicit Types κ : lft.
+
+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' [? ->]].
+  by move=> /Some_pair_included [_] /Some_included_total /DecAgree_included=>->.
+Qed.
+
+(** Ownership *)
+Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
+  own_ilft_auth I -∗
+    own ilft_name (◯ {[κ := DecAgree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
+Proof.
+  iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
+    as %[[? [??]]%singleton_included _]%auth_valid_discrete_2.
+  unfold to_ilftUR in *. simplify_map_eq; simplify_option_eq; eauto.
+Qed.
+
+Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
+  own_alft_auth A -∗
+    own alft_name (◯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some b⌝.
+Proof.
+  iIntros "HA HΛ".
+  iDestruct (own_valid_2 with "HA HΛ") as %[HA _]%auth_valid_discrete_2.
+  iPureIntro. move: HA=> /singleton_included [qs [/leibniz_equiv_iff]].
+  rewrite lookup_fmap fmap_Some=> -[b' [? ->]] /Some_included.
+  move=> [/leibniz_equiv_iff|/csum_included]; destruct b, b'; naive_solver.
+Qed.
+
+Lemma own_bor_auth I κ x : own_ilft_auth I -∗ own_bor κ x -∗ ⌜is_Some (I !! κ)⌝.
+Proof.
+  iIntros "HI"; iDestruct 1 as (γs) "[? _]".
+  by iApply (own_ilft_auth_agree with "HI").
+Qed.
+Lemma own_bor_op κ x y : own_bor κ (x ⋅ y) ⊣⊢ own_bor κ x ∗ own_bor κ y.
+Proof.
+  iSplit.
+  { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
+  iIntros "[Hx Hy]".
+  iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
+  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
+  iExists γs. iSplit. done. rewrite own_op; iFrame.
+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).
+Proof. apply wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
+Lemma own_bor_update κ x y : x ~~> y → own_bor κ x ==∗ own_bor κ y.
+Proof.
+  iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
+Qed.
+Lemma own_bor_update_2 κ x1 x2 y :
+  x1 ⋅ x2 ~~> y → own_bor κ x1 ⊢ own_bor κ x2 ==∗ own_bor κ y.
+Proof.
+  intros. apply wand_intro_r. rewrite -own_bor_op. by apply own_bor_update.
+Qed.
+
+Lemma own_cnt_auth I κ x : own_ilft_auth I -∗ own_cnt κ x -∗ ⌜is_Some (I !! κ)⌝.
+Proof.
+  iIntros "HI"; iDestruct 1 as (γs) "[? _]".
+  by iApply (own_ilft_auth_agree with "HI").
+Qed.
+Lemma own_cnt_op κ x y : own_cnt κ (x ⋅ y) ⊣⊢ own_cnt κ x ∗ own_cnt κ y.
+Proof.
+  iSplit.
+  { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
+  iIntros "[Hx Hy]".
+  iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
+  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
+  iExists γs. iSplit; first done. rewrite own_op; iFrame.
+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).
+Proof. apply wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
+Lemma own_cnt_update κ x y : x ~~> y → own_cnt κ x ==∗ own_cnt κ y.
+Proof.
+  iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
+Qed.
+Lemma own_cnt_update_2 κ x1 x2 y :
+  x1 ⋅ x2 ~~> y → own_cnt κ x1 -∗ own_cnt κ x2 ==∗ own_cnt κ y.
+Proof.
+  intros. apply wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
+Qed.
+
+Lemma own_inh_auth I κ x : own_ilft_auth I -∗ own_inh κ x -∗ ⌜is_Some (I !! κ)⌝.
+Proof.
+  iIntros "HI"; iDestruct 1 as (γs) "[? _]".
+  by iApply (own_ilft_auth_agree with "HI").
+Qed.
+Lemma own_inh_op κ x y : own_inh κ (x ⋅ y) ⊣⊢ own_inh κ x ∗ own_inh κ y.
+Proof.
+  iSplit.
+  { iDestruct 1 as (γs) "[#? [Hx Hy]]"; iSplitL "Hx"; iExists γs; eauto. }
+  iIntros "[Hx Hy]".
+  iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
+  iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs%auth_own_valid.
+  move: Hγs; rewrite /= op_singleton singleton_valid=> /dec_agree_op_inv [<-].
+  iExists γs. iSplit. done. rewrite own_op; iFrame.
+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).
+Proof. apply wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
+Lemma own_inh_update κ x y : x ~~> y → own_inh κ x ==∗ own_inh κ y.
+Proof.
+  iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
+Qed.
+Lemma own_inh_update_2 κ x1 x2 y :
+  x1 ⋅ x2 ~~> y → own_inh κ x1 ⊢ own_inh κ x2 ==∗ own_inh κ y.
+Proof.
+  intros. apply wand_intro_r. rewrite -own_inh_op. by apply own_inh_update.
+Qed.
+
+(** Alive and dead *)
+Global Instance lft_alive_in_dec A κ : Decision (lft_alive_in A κ).
+Proof.
+  refine (cast_if (decide (set_Forall (λ Λ, A !! Λ = Some true)
+                  (dom (gset atomic_lft) κ))));
+    rewrite /lft_alive_in; by setoid_rewrite <-gmultiset_elem_of_dom.
+Qed.
+Global Instance lft_dead_in_dec A κ : Decision (lft_dead_in A κ).
+Proof.
+  refine (cast_if (decide (set_Exists (λ Λ, A !! Λ = Some false)
+                  (dom (gset atomic_lft) κ))));
+      rewrite /lft_dead_in; by setoid_rewrite <-gmultiset_elem_of_dom.
+Qed.
+
+Lemma lft_alive_or_dead_in A κ :
+  (∃ Λ, Λ ∈ κ ∧ A !! Λ = None) ∨ (lft_alive_in A κ ∨ lft_dead_in A κ).
+Proof.
+  rewrite /lft_alive_in /lft_dead_in.
+  destruct (decide (set_Exists (λ Λ, A !! Λ = None) (dom (gset _) κ)))
+    as [(Λ & ?%gmultiset_elem_of_dom & HAΛ)|HA%(not_set_Exists_Forall _)]; first eauto.
+  destruct (decide (set_Exists (λ Λ, A !! Λ = Some false) (dom (gset _) κ)))
+    as [(Λ & HΛ%gmultiset_elem_of_dom & ?)|HA'%(not_set_Exists_Forall _)]; first eauto.
+  right; left. intros Λ HΛ%gmultiset_elem_of_dom.
+  move: (HA _ HΛ) (HA' _ HΛ)=> /=. case: (A !! Λ)=>[[]|]; naive_solver.
+Qed.
+Lemma lft_alive_and_dead_in A κ : lft_alive_in A κ → lft_dead_in A κ → False.
+Proof. intros Halive (Λ&HΛ&?). generalize (Halive _ HΛ). naive_solver. Qed.
+
+Lemma lft_alive_in_subseteq A κ κ' :
+  lft_alive_in A κ → κ' ⊆ κ → lft_alive_in A κ'.
+Proof. intros Halive ? Λ ?. by eapply Halive, gmultiset_elem_of_subseteq. Qed.
+
+Lemma lft_alive_in_insert A κ Λ b :
+  A !! Λ = None → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
+Proof.
+  intros HΛ Halive Λ' HΛ'.
+  assert (Λ ≠ Λ') by (intros ->; move:(Halive _ HΛ'); by rewrite HΛ).
+  rewrite lookup_insert_ne; eauto.
+Qed.
+Lemma lft_alive_in_insert_false A κ Λ b :
+  Λ ∉ κ → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
+Proof.
+  intros HΛ Halive Λ' HΛ'.
+  rewrite lookup_insert_ne; last (by intros ->); auto.
+Qed.
+
+Lemma lft_dead_in_insert A κ Λ b :
+  A !! Λ = None → lft_dead_in A κ → lft_dead_in (<[Λ:=b]> A) κ.
+Proof.
+  intros HΛ (Λ'&?&HΛ').
+  assert (Λ ≠ Λ') by (intros ->; move:HΛ'; by rewrite HΛ).
+  exists Λ'. by rewrite lookup_insert_ne.
+Qed.
+Lemma lft_dead_in_insert_false A κ Λ :
+  lft_dead_in A κ → lft_dead_in (<[Λ:=false]> A) κ.
+Proof.
+  intros (Λ'&?&HΛ'). destruct (decide (Λ = Λ')) as [<-|].
+  - exists Λ. by rewrite lookup_insert.
+  - exists Λ'. by rewrite lookup_insert_ne.
+Qed.
+Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
+Proof. exists Λ. by rewrite lookup_insert. Qed.
+
+Lemma lft_inv_alive_twice κ : lft_inv_alive κ -∗ lft_inv_alive κ -∗ False.
+Proof.
+  rewrite lft_inv_alive_unfold /lft_inh.
+  iDestruct 1 as (P Q) "(_&_&Hinh)"; iDestruct 1 as (P' Q') "(_&_&Hinh')".
+  iDestruct "Hinh" as (E) "[HE _]"; iDestruct "Hinh'" as (E') "[HE' _]".
+  by iDestruct (own_inh_valid_2 with "HE HE'") as %?.
+Qed.
+
+Lemma lft_inv_alive_in A κ : lft_alive_in A κ → lft_inv A κ -∗ lft_inv_alive κ.
+Proof.
+  rewrite /lft_inv. iIntros (?) "[[$ _]|[_ %]]".
+  by destruct (lft_alive_and_dead_in A κ).
+Qed.
+Lemma lft_inv_dead_in A κ : lft_dead_in A κ → lft_inv A κ -∗ lft_inv_dead κ.
+Proof.
+  rewrite /lft_inv. iIntros (?) "[[_ %]|[$ _]]".
+  by destruct (lft_alive_and_dead_in A κ).
+Qed.
+
+(** Basic rules about lifetimes  *)
+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].
+Proof.
+  rewrite /lft_dead -or_exist. apply exist_proper=> Λ.
+  rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
+Qed.
+
+Lemma lft_tok_dead q κ : q.[κ] -∗ [† κ] -∗ False.
+Proof.
+  rewrite /lft_tok /lft_dead. iIntros "H"; iDestruct 1 as (Λ') "[% H']".
+  iDestruct (big_sepMS_elem_of _ _ Λ' with "H") as "H"=> //.
+  iDestruct (own_valid_2 with "H H'") as %Hvalid.
+  move: Hvalid=> /auth_own_valid /=; by rewrite op_singleton singleton_valid.
+Qed.
+
+Lemma lft_tok_static q : q.[static]%I.
+Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
+
+Lemma lft_dead_static : [† static] -∗ False.
+Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
+
+(* Fractional and AsFractional instances *)
+Global Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
+Proof.
+  intros p q. rewrite /lft_tok -big_sepMS_sepMS. apply big_sepMS_proper.
+  intros Λ ?. rewrite -Cinl_op -op_singleton auth_frag_op own_op //.
+Qed.
+Global Instance lft_tok_as_fractional κ q :
+  AsFractional q.[κ] (λ q, q.[κ])%I q.
+Proof. done. Qed.
+Global Instance idx_bor_own_fractional i : Fractional (λ q, idx_bor_own q i)%I.
+Proof.
+  intros p q. rewrite /idx_bor_own -own_bor_op /own_bor. f_equiv=>?.
+  by rewrite -auth_frag_op op_singleton.
+Qed.
+Global Instance idx_bor_own_as_fractional i q :
+  AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
+Proof. done. Qed.
+
+(** Lifetime inclusion *)
+Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
+Proof.
+  iIntros (->%gmultiset_union_difference) "!#". iSplitR.
+  - 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.
+
+Lemma lft_incl_refl κ : (κ ⊑ κ)%I.
+Proof. by apply lft_le_incl. Qed.
+
+Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
+Proof.
+  rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†] !#". iSplitR.
+  - iIntros (q) "Hκ".
+    iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
+    iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
+    iExists q''. iIntros "{$Hκ''} !> Hκ''".
+    iMod ("Hclose'" with "Hκ''") as "Hκ'". by iApply "Hclose".
+  - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
+Qed.
+
+Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
+Proof.
+  unfold 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]".
+    iMod ("Hclose'" with "[$Hκ' $Hκ'0]") as "$".
+    iApply "Hclose''". iFrame.
+  - 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/lifetime/rebor.v b/theories/lifetime/rebor.v
new file mode 100644
index 0000000000000000000000000000000000000000..bba7edeeb34ad2a867db6b5913015c6c76ad7dc6
--- /dev/null
+++ b/theories/lifetime/rebor.v
@@ -0,0 +1,160 @@
+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/shr_borrow.v b/theories/lifetime/shr_borrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..4f5042ef4c7e63c05d7cb32aea0fd79835dd8461
--- /dev/null
+++ b/theories/lifetime/shr_borrow.v
@@ -0,0 +1,56 @@
+From iris.algebra Require Import gmap auth frac.
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Export derived.
+
+(** Shared bors  *)
+Definition shr_bor `{invG Σ, lftG Σ} κ (P : iProp Σ) :=
+  (∃ i, &{κ,i}P ∗ inv lftN (∃ q, idx_bor_own q i))%I.
+Notation "&shr{ κ } P" := (shr_bor κ P)
+  (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
+
+Section shared_bors.
+  Context `{invG Σ, lftG Σ} (P : iProp Σ).
+
+  Global Instance shr_bor_proper :
+    Proper ((⊣⊢) ==> (⊣⊢)) (shr_bor κ).
+  Proof. solve_proper. Qed.
+  Global Instance shr_bor_persistent : PersistentP (&shr{κ} P) := _.
+
+  Lemma bor_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
+  Proof.
+    iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
+    iExists i. iFrame "#". iApply inv_alloc. auto.
+  Qed.
+
+  Lemma shr_bor_acc E κ :
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
+               [†κ] ∗ |={E∖↑lftN,E}=> True.
+  Proof.
+    iIntros (?) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
+    iInv lftN as (q') ">[Hq'0 Hq'1]" "Hclose".
+    iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
+    iMod (idx_bor_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
+    - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
+    - iRight. iFrame. iIntros "!>". by iMod "Hclose".
+  Qed.
+
+  Lemma shr_bor_acc_tok E q κ :
+    ↑lftN ⊆ E →
+    lft_ctx -∗ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
+  Proof.
+    iIntros (?) "#LFT #Hshr Hκ".
+    iMod (shr_bor_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]". done.
+    - iIntros "!>HP". by iMod ("Hclose" with "HP").
+    - iDestruct (lft_tok_dead with "Hκ H†") as "[]".
+  Qed.
+
+  Lemma shr_bor_shorten κ κ': κ ⊑ κ' -∗ &shr{κ'}P -∗ &shr{κ}P.
+  Proof.
+    iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+      by iApply (idx_bor_shorten with "H⊑").
+  Qed.
+
+End shared_bors.
+
+Typeclasses Opaque shr_bor.
diff --git a/theories/lifetime/tl_borrow.v b/theories/lifetime/tl_borrow.v
new file mode 100644
index 0000000000000000000000000000000000000000..5770fc4e07a35387bd93af4d9b7b99f5c0e87633
--- /dev/null
+++ b/theories/lifetime/tl_borrow.v
@@ -0,0 +1,51 @@
+From lrust.lifetime Require Export derived.
+From iris.base_logic.lib Require Export thread_local.
+From iris.proofmode Require Import tactics.
+
+Definition tl_bor `{invG Σ, lftG Σ, thread_localG Σ}
+           (κ : lft) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
+  (∃ i, &{κ,i}P ∗ tl_inv tid N (idx_bor_own 1 i))%I.
+
+Notation "&tl{ κ , tid , N } P" := (tl_bor κ tid N P)
+  (format "&tl{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
+
+Section tl_bor.
+  Context `{invG Σ, lftG Σ, thread_localG Σ}
+          (tid : thread_id) (N : namespace) (P : iProp Σ).
+
+  Global Instance tl_bor_persistent κ : PersistentP (&tl{κ,tid,N} P) := _.
+  Global Instance tl_bor_proper κ :
+    Proper ((⊣⊢) ==> (⊣⊢)) (tl_bor κ tid N).
+  Proof.
+    intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
+  Qed.
+
+  Lemma bor_tl κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &tl{κ,tid,N}P.
+  Proof.
+    iIntros (?) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "[#? Hown]".
+    iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
+  Qed.
+
+  Lemma tl_bor_acc q κ E F :
+    ↑lftN ⊆ E → ↑tlN ⊆ E → ↑N ⊆ F →
+    lft_ctx -∗ &tl{κ,tid,N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
+            ▷P ∗ tl_own tid (F ∖ ↑N) ∗
+            (▷P -∗ tl_own tid (F ∖ ↑N) ={E}=∗ q.[κ] ∗ tl_own tid F).
+  Proof.
+    iIntros (???) "#LFT#HP Hκ Htlown".
+    iDestruct "HP" as (i) "(#Hpers&#Hinv)".
+    iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done.
+    iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
+    iIntros "{$HP $Htlown}!>HP Htlown".
+    iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
+  Qed.
+
+  Lemma tl_bor_shorten κ κ': κ ⊑ κ' -∗ &tl{κ',tid,N}P -∗ &tl{κ,tid,N}P.
+  Proof.
+    iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
+    iApply (idx_bor_shorten with "Hκκ' H").
+  Qed.
+
+End tl_bor.
+
+Typeclasses Opaque tl_bor.
diff --git a/theories/shr_borrow.v b/theories/shr_borrow.v
deleted file mode 100644
index 5987de8da012e84c88c41313c7e049e2d33d515e..0000000000000000000000000000000000000000
--- a/theories/shr_borrow.v
+++ /dev/null
@@ -1,57 +0,0 @@
-From iris.algebra Require Import gmap auth frac.
-From iris.proofmode Require Import tactics.
-From lrust Require Export lifetime.
-
-(** Shared borrows  *)
-Definition shr_borrow `{invG Σ, lifetimeG Σ} κ (P : iProp Σ) :=
-  (∃ i, idx_borrow κ i P ∗ inv lftN (∃ q, idx_borrow_own q i))%I.
-Notation "&shr{ κ } P" := (shr_borrow κ P)
-  (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
-
-Section shared_borrows.
-  Context `{invG Σ, lifetimeG Σ} (P : iProp Σ).
-
-  Global Instance shr_borrow_proper :
-    Proper ((⊣⊢) ==> (⊣⊢)) (shr_borrow κ).
-  Proof. solve_proper. Qed.
-  Global Instance shr_borrow_persistent : PersistentP (&shr{κ} P) := _.
-
-  Lemma borrow_share E κ : ↑lftN ⊆ E → &{κ}P ={E}=∗ &shr{κ}P.
-  Proof.
-    iIntros (?) "HP". unfold borrow. iDestruct "HP" as (i) "(#?&Hown)".
-    iExists i. iFrame "#". iApply inv_alloc. auto.
-  Qed.
-
-  Lemma shr_borrow_acc E κ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &shr{κ}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
-               [†κ] ∗ |={E∖↑lftN,E}=> True.
-  Proof.
-    iIntros (?) "#LFT #HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)".
-    iInv lftN as (q') ">Hq'" "Hclose".
-    rewrite -(Qp_div_2 q') /idx_borrow_own -op_singleton auth_frag_op own_op.
-    iDestruct "Hq'" as "[Hq'0 Hq'1]". iMod ("Hclose" with "[Hq'1]") as "_". by eauto.
-    iMod (idx_borrow_atomic_acc with "LFT Hidx Hq'0") as "[[HP Hclose]|[H† Hclose]]". done.
-    - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iRight. iFrame. iIntros "!>". by iMod "Hclose".
-  Qed.
-
-  Lemma shr_borrow_acc_tok E q κ :
-    ↑lftN ⊆ E →
-    lft_ctx -∗ &shr{κ}P -∗ q.[κ] ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ q.[κ]).
-  Proof.
-    iIntros (?) "#LFT #Hshr Hκ".
-    iMod (shr_borrow_acc with "LFT Hshr") as "[[$ Hclose]|[H† _]]". done.
-    - iIntros "!>HP". by iMod ("Hclose" with "HP").
-    - iDestruct (lft_own_dead with "Hκ H†") as "[]".
-  Qed.
-
-  Lemma shr_borrow_shorten κ κ': κ ⊑ κ' -∗ &shr{κ'}P -∗ &shr{κ}P.
-  Proof.
-    iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
-      by iApply (idx_borrow_shorten with "H⊑").
-  Qed.
-
-End shared_borrows.
-
-Typeclasses Opaque shr_borrow.
diff --git a/theories/tl_borrow.v b/theories/tl_borrow.v
deleted file mode 100644
index 3b78fb28d79b23d4d2f85bf40fca93b8a3cc553d..0000000000000000000000000000000000000000
--- a/theories/tl_borrow.v
+++ /dev/null
@@ -1,51 +0,0 @@
-From lrust Require Export lifetime.
-From iris.base_logic.lib Require Export thread_local.
-From iris.proofmode Require Import tactics.
-
-Definition tl_borrow `{invG Σ, lifetimeG Σ, thread_localG Σ}
-           (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
-  (∃ i, idx_borrow κ i P ∗ tl_inv tid N (idx_borrow_own 1 i))%I.
-
-Notation "&tl{ κ | tid | N } P" := (tl_borrow κ tid N P)
-  (format "&tl{ κ | tid | N } P", at level 20, right associativity) : uPred_scope.
-
-Section tl_borrow.
-  Context `{invG Σ, lifetimeG Σ, thread_localG Σ}
-          (tid : thread_id) (N : namespace) (P : iProp Σ).
-
-  Global Instance tl_borrow_persistent κ : PersistentP (&tl{κ|tid|N} P) := _.
-  Global Instance tl_borrow_proper κ :
-    Proper ((⊣⊢) ==> (⊣⊢)) (tl_borrow κ tid N).
-  Proof.
-    intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
-  Qed.
-
-  Lemma borrow_tl κ E : ↑lftN ⊆ E → &{κ}P ={E}=∗ &tl{κ|tid|N}P.
-  Proof.
-    iIntros (?) "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
-    iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
-  Qed.
-
-  Lemma tl_borrow_acc q κ E F :
-    ↑lftN ⊆ E → ↑tlN ⊆ E → ↑N ⊆ F →
-    lft_ctx -∗ &tl{κ|tid|N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
-            ▷P ∗ tl_own tid (F ∖ ↑N) ∗
-            (▷P -∗ tl_own tid (F ∖ ↑N) ={E}=∗ q.[κ] ∗ tl_own tid F).
-  Proof.
-    iIntros (???) "#LFT#HP Hκ Htlown".
-    iDestruct "HP" as (i) "(#Hpers&#Hinv)".
-    iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done.
-    iMod (idx_borrow_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
-    iIntros "{$HP $Htlown}!>HP Htlown".
-    iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
-  Qed.
-
-  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' -∗ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
-  Proof.
-    iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
-    iApply (idx_borrow_shorten with "Hκκ' H").
-  Qed.
-
-End tl_borrow.
-
-Typeclasses Opaque tl_borrow.
diff --git a/theories/perm.v b/theories/typing/perm.v
similarity index 89%
rename from theories/perm.v
rename to theories/typing/perm.v
index ae364946073f7bd5797991f96d897acd2c3843ed..7e88e51a27fd4afcc50f1b6ff08bf6cbfb6e83e9 100644
--- a/theories/perm.v
+++ b/theories/typing/perm.v
@@ -1,5 +1,7 @@
 From iris.proofmode Require Import tactics.
-From lrust Require Export type proofmode.
+From lrust.typing Require Export type.
+From lrust.lang Require Export proofmode.
+From lrust.lifetime Require Import frac_borrow.
 
 Delimit Scope perm_scope with P.
 Bind Scope perm_scope with perm.
@@ -23,17 +25,17 @@ Section perm.
   Definition has_type (ν : expr) (ty : type) : perm := λ tid,
     from_option (λ v, ty.(ty_own) tid [v]) False%I (eval_expr ν).
 
-  Definition extract (κ : lifetime) (ρ : perm) : perm :=
+  Definition extract (κ : lft) (ρ : perm) : perm :=
     λ tid, ([†κ] ={↑lftN}=∗ ρ tid)%I.
 
-  Definition tok (κ : lifetime) (q : Qp) : perm :=
+  Definition tok (κ : lft) (q : Qp) : perm :=
     λ _, q.[κ]%I.
 
 
-  Definition killable (κ : lifetime) : perm :=
+  Definition killable (κ : lft) : perm :=
     λ _, (□ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]))%I.
 
-  Definition incl (κ κ' : lifetime) : perm :=
+  Definition incl (κ κ' : lft) : perm :=
     λ _, (κ ⊑ κ')%I.
 
   Definition exist {A : Type} (P : A -> perm) : @perm Σ :=
@@ -61,7 +63,7 @@ Notation "q .[ κ ]" := (tok κ q) (format "q .[ κ ]", at level 0) : perm_scope
 
 Notation "† κ" := (killable κ) (format "† κ", at level 75).
 
-Infix "⊑" := incl (at level 60) : perm_scope.
+Infix "⊑" := incl (at level 70) : perm_scope.
 
 Notation "∃ x .. y , P" :=
   (exist (λ x, .. (exist (λ y, P)) ..)) : perm_scope.
diff --git a/theories/perm_incl.v b/theories/typing/perm_incl.v
similarity index 93%
rename from theories/perm_incl.v
rename to theories/typing/perm_incl.v
index ff589d0e07b642e47a02b056df9dc9e5a5dd8459..8791ec050e943875fbfa01102529372ddd6f6d37 100644
--- a/theories/perm_incl.v
+++ b/theories/typing/perm_incl.v
@@ -1,6 +1,7 @@
 From Coq Require Import Qcanon.
 From iris.base_logic Require Import big_op.
-From lrust Require Export type perm.
+From lrust.typing Require Export type perm.
+From lrust.lifetime Require Import frac_borrow.
 
 Import Perm Types.
 
@@ -191,7 +192,7 @@ Section props.
         * etransitivity. apply IHl. by injection Hlen. do 3 f_equiv. lia.
   Qed.
 
-  Lemma perm_split_uniq_borrow_prod2 ty1 ty2 κ ν :
+  Lemma perm_split_uniq_bor_prod2 ty1 ty2 κ ν :
     ν ◁ &uniq{κ} (product2 ty1 ty2) ⇒
     ν ◁ &uniq{κ} ty1 ∗ ν +ₗ #(ty1.(ty_size)) ◁ &uniq{κ} ty2.
   Proof.
@@ -199,11 +200,11 @@ Section props.
     destruct (eval_expr ν) as [[[|l|]|]|];
       iIntros (tid) "#LFT H"; try iDestruct "H" as "[]";
         iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=<-].
-    rewrite /= split_prod_mt. iMod (borrow_split with "LFT H") as "[H1 H2]".
+    rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]".
     set_solver. iSplitL "H1"; eauto.
   Qed.
 
-  Lemma perm_split_uniq_borrow_prod tyl κ ν :
+  Lemma perm_split_uniq_bor_prod tyl κ ν :
     ν ◁ &uniq{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
              ν +ₗ #(tyoffs.2:nat) ◁ &uniq{κ} (tyoffs.1) ∗ acc)%P
@@ -214,12 +215,12 @@ Section props.
       iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->].
       rewrite shift_loc_0 /=. eauto. }
     generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "_ H/=".
-    etransitivity. apply perm_split_uniq_borrow_prod2.
+    etransitivity. apply perm_split_uniq_bor_prod2.
     iIntros (tid) "#LFT /=[$ H]". iApply (IH with "LFT"). rewrite /has_type /=.
     destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat.
   Qed.
 
-  Lemma perm_split_shr_borrow_prod2 ty1 ty2 κ ν :
+  Lemma perm_split_shr_bor_prod2 ty1 ty2 κ ν :
     ν ◁ &shr{κ} (product2 ty1 ty2) ⇒
     ν ◁ &shr{κ} ty1 ∗ ν +ₗ #(ty1.(ty_size)) ◁ &shr{κ} ty2.
   Proof.
@@ -233,7 +234,7 @@ Section props.
     set_solver. iApply lft_incl_refl. set_solver. iApply lft_incl_refl.
   Qed.
 
-  Lemma perm_split_shr_borrow_prod tyl κ ν :
+  Lemma perm_split_shr_bor_prod tyl κ ν :
     ν ◁ &shr{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
              (ν +ₗ #(tyoffs.2:nat))%E ◁ &shr{κ} (tyoffs.1) ∗ acc)%P
@@ -244,12 +245,12 @@ Section props.
       iDestruct "H" as (l) "[Heq H]". iDestruct "Heq" as %[=->].
       rewrite shift_loc_0 /=. iExists _. by iFrame "∗%". }
     generalize 0%nat. induction tyl as [|ty tyl IH]=>offs. by iIntros (tid) "_ H/=".
-    etransitivity. apply perm_split_shr_borrow_prod2.
+    etransitivity. apply perm_split_shr_bor_prod2.
     iIntros (tid) "#LFT /=[$ H]". iApply (IH with "LFT"). rewrite /has_type /=.
     destruct (eval_expr ν) as [[[]|]|]=>//=. by rewrite shift_loc_assoc_nat.
   Qed.
 
-  Lemma reborrow_shr_perm_incl κ κ' ν ty :
+  Lemma rebor_shr_perm_incl κ κ' ν ty :
     κ ⊑ κ' ∗ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
   Proof.
     iIntros (tid) "#LFT [#Hord #Hκ']". unfold has_type.
@@ -274,15 +275,15 @@ Section props.
       try by (iDestruct "Hown" as "[]" || iDestruct "Hown" as (l) "[% _]").
     iDestruct "Hown" as (l') "[EQ [Hown Hf]]". iDestruct "EQ" as %[=]. subst l'.
     iApply (fupd_mask_mono (↑lftN)). done.
-    iMod (borrow_create with "LFT Hown") as "[Hbor Hext]". done.
+    iMod (bor_create with "LFT Hown") as "[Hbor Hext]". done.
     iSplitL "Hbor". by simpl; eauto.
-    iMod (borrow_create with "LFT Hf") as "[_ Hf]". done.
+    iMod (bor_create with "LFT Hf") as "[_ Hf]". done.
     iIntros "!>#H†".
     iMod ("Hext" with "H†") as "Hext". iMod ("Hf" with "H†") as "Hf". iIntros "!>/=".
     iExists _. iFrame. auto.
   Qed.
 
-  Lemma reborrow_uniq_borrowing κ κ' ν ty :
+  Lemma rebor_uniq_borrowing κ κ' ν ty :
     borrowing κ (κ ⊑ κ') (ν ◁ &uniq{κ'}ty) (ν ◁ &uniq{κ}ty).
   Proof.
     iIntros (tid) "#LFT #Hord H". unfold has_type.
@@ -290,7 +291,7 @@ Section props.
       try by (iDestruct "H" as "[]" || iDestruct "H" as (l) "[% _]").
     iDestruct "H" as (l') "[EQ H]". iDestruct "EQ" as %[=]. subst l'.
     iApply (fupd_mask_mono (↑lftN)). done.
-    iMod (reborrow with "LFT Hord H") as "[H Hextr]". done.
+    iMod (rebor with "LFT Hord H") as "[H Hextr]". done.
     iModIntro. iSplitL "H". iExists _. by eauto.
     iIntros "H†". iMod ("Hextr" with "H†"). simpl. auto.
   Qed.
@@ -298,10 +299,10 @@ Section props.
   Lemma lftincl_borrowing κ κ' q : borrowing κ ⊤ q.[κ'] (κ ⊑ κ').
   Proof.
     iIntros (tid) "#LFT _ Htok". iApply (fupd_mask_mono (↑lftN)). done.
-    iMod (borrow_create with "LFT [$Htok]") as "[Hbor Hclose]". done.
-    iMod (borrow_fracture (λ q', (q * q').[κ'])%I with "LFT [Hbor]") as "Hbor". done.
+    iMod (bor_create with "LFT [$Htok]") as "[Hbor Hclose]". done.
+    iMod (bor_fracture (λ q', (q * q').[κ'])%I with "LFT [Hbor]") as "Hbor". done.
     { by rewrite Qp_mult_1_r. }
-    iSplitL "Hbor". iApply (frac_borrow_incl with "LFT Hbor").
+    iSplitL "Hbor". iApply (frac_bor_incl with "LFT Hbor").
     iIntros "!>H". by iMod ("Hclose" with "H") as ">$".
   Qed.
 
diff --git a/theories/type.v b/theories/typing/type.v
similarity index 83%
rename from theories/type.v
rename to theories/typing/type.v
index 21b23768763691738926f3dee9381080c1734e70..8f3bdd31ca2fa2e440b8322bb3162b197789f1aa 100644
--- a/theories/type.v
+++ b/theories/typing/type.v
@@ -2,13 +2,14 @@ From Coq Require Import Qcanon.
 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 Require Export notation lifetime frac_borrow heap.
+From lrust.lang Require Export heap notation.
+From lrust.lifetime Require Import frac_borrow.
 
 Class iris_typeG Σ := Iris_typeG {
   type_heapG :> heapG Σ;
-  type_lifetimeG :> lifetimeG Σ;
+  type_lftG :> lftG Σ;
   type_thread_localG :> thread_localG Σ;
-  type_frac_borrowG Σ :> frac_borrowG Σ
+  type_frac_borrowG Σ :> frac_borG Σ
 }.
 
 Definition mgmtE := ↑tlN ∪ ↑lftN.
@@ -25,7 +26,7 @@ Record type :=
   { ty_size : nat;
     ty_dup : bool;
     ty_own : thread_id → list val → iProp Σ;
-    ty_shr : lifetime → thread_id → coPset → loc → iProp Σ;
+    ty_shr : lft → thread_id → coPset → loc → iProp Σ;
 
     ty_dup_persistent tid vl : ty_dup → PersistentP (ty_own tid vl);
     ty_shr_persistent κ tid E l : PersistentP (ty_shr κ tid E l);
@@ -76,22 +77,22 @@ Program Coercion ty_of_st (st : simple_type) : type :=
 Next Obligation. intros. apply st_size_eq. Qed.
 Next Obligation.
   intros st E N κ l tid q ? ?. iIntros "#LFT Hmt Htok".
-  iMod (borrow_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
-  iMod (borrow_split with "LFT Hmt") as "[Hmt Hown]". set_solver.
-  iMod (borrow_persistent with "LFT Hown Htok") as "[Hown $]". set_solver.
-  iMod (borrow_fracture with "LFT [Hmt]") as "Hfrac"; last first.
+  iMod (bor_exists with "LFT Hmt") as (vl) "Hmt". set_solver.
+  iMod (bor_sep with "LFT Hmt") as "[Hmt Hown]". set_solver.
+  iMod (bor_persistent with "LFT Hown Htok") as "[Hown $]". set_solver.
+  iMod (bor_fracture with "LFT [Hmt]") as "Hfrac"; last first.
   { iExists vl. by iFrame. }
   done. set_solver.
 Qed.
 Next Obligation.
   intros st κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
   iDestruct "H" as (vl) "[Hf Hown]".
-  iExists vl. iFrame. by iApply (frac_borrow_shorten with "Hord").
+  iExists vl. iFrame. by iApply (frac_bor_shorten with "Hord").
 Qed.
 Next Obligation.
   intros st κ tid E F l q ??. iIntros "#LFT #Hshr[Hlft $]".
   iDestruct "Hshr" as (vl) "[Hf Hown]".
-  iMod (frac_borrow_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
+  iMod (frac_bor_acc with "LFT Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver.
   iModIntro. iExists _. iDestruct "Hmt" as "[Hmt1 Hmt2]". iSplitL "Hmt1".
   - iNext. iExists _. by iFrame.
   - iIntros "Hmt1". iDestruct "Hmt1" as (vl') "[Hmt1 #Hown']".
@@ -125,9 +126,9 @@ Section types.
   Next Obligation. iIntros (tid vl) "[]". Qed.
   Next Obligation.
     iIntros (????????) "#LFT Hb Htok".
-    iMod (borrow_exists with "LFT Hb") as (vl) "Hb". set_solver.
-    iMod (borrow_split with "LFT Hb") as "[_ Hb]". set_solver.
-    iMod (borrow_persistent with "LFT Hb Htok") as "[>[] _]". set_solver.
+    iMod (bor_exists with "LFT Hb") as (vl) "Hb". set_solver.
+    iMod (bor_sep with "LFT Hb") as "[_ Hb]". set_solver.
+    iMod (bor_persistent with "LFT Hb Htok") as "[>[] _]". set_solver.
   Qed.
   Next Obligation. intros. iIntros "_ _ []". Qed.
   Next Obligation. intros. iIntros "_ []". Qed.
@@ -164,34 +165,32 @@ Section types.
   Qed.
   Next Obligation.
     move=> q ty E N κ l tid q' ?? /=. iIntros "#LFT Hshr Htok".
-    iMod (borrow_exists with "LFT Hshr") as (vl) "Hb". set_solver.
-    iMod (borrow_split with "LFT Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (borrow_exists with "LFT Hb2") as (l') "Hb2". set_solver.
-    iMod (borrow_split with "LFT Hb2") as "[EQ Hb2]". set_solver.
-    iMod (borrow_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
+    iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
+    iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
+    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
+    iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
+    iMod (bor_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
-    iMod (borrow_split with "LFT Hb2") as "[Hb2 _]". set_solver.
-    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
-    rewrite /borrow. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
-    iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
+    iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
+    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
+    rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
+    iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty κ tid (↑N) l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
     iExists l'. iIntros "!>{$Hbf}".  iIntros (q'') "!#Htok".
     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".
-      { rewrite /borrow. iExists i. eauto. }
-      iMod (borrow_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.
+    - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hb". set_solver.
+      { rewrite bor_unfold_idx. iExists i. 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.
     intros _ ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
     iDestruct "H" as (l') "[Hfb Hvs]".
-    iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]").
+    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
     iIntros (q') "!#Htok".
     iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
     iMod (lft_incl_acc with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
@@ -202,14 +201,14 @@ Section types.
   Qed.
   Next Obligation. done. Qed.
 
-  Program Definition uniq_borrow (κ:lifetime) (ty:type) :=
+  Program Definition uniq_bor (κ:lft) (ty:type) :=
     {| ty_size := 1; ty_dup := false;
        ty_own tid vl :=
          (∃ l:loc, ⌜vl = [ #l ]⌝ ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
        ty_shr κ' tid E l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
-            ∀ q', □ (q'.[κ ⋅ κ']
-               ={mgmtE ∪ E, ↑tlN}▷=∗ ty.(ty_shr) (κ⋅κ') tid E l' ∗ q'.[κ⋅κ']))%I
+            ∀ q', □ (q'.[κ∪κ']
+               ={mgmtE ∪ E, ↑tlN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q'.[κ∪κ']))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -217,15 +216,15 @@ Section types.
   Qed.
   Next Obligation.
     move=> κ ty E N κ' l tid q' ??/=. iIntros "#LFT Hshr Htok".
-    iMod (borrow_exists with "LFT Hshr") as (vl) "Hb". set_solver.
-    iMod (borrow_split with "LFT Hb") as "[Hb1 Hb2]". set_solver.
-    iMod (borrow_exists with "LFT Hb2") as (l') "Hb2". set_solver.
-    iMod (borrow_split with "LFT Hb2") as "[EQ Hb2]". set_solver.
-    iMod (borrow_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
+    iMod (bor_exists with "LFT Hshr") as (vl) "Hb". set_solver.
+    iMod (bor_sep with "LFT Hb") as "[Hb1 Hb2]". set_solver.
+    iMod (bor_exists with "LFT Hb2") as (l') "Hb2". set_solver.
+    iMod (bor_sep with "LFT Hb2") as "[EQ Hb2]". set_solver.
+    iMod (bor_persistent with "LFT EQ Htok") as "[>% $]". set_solver. subst.
     rewrite heap_mapsto_vec_singleton.
-    iMod (borrow_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
-    rewrite {1}/borrow. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
-    iMod (inv_alloc N _ (idx_borrow_own 1 i ∨ ty_shr ty (κ⋅κ') tid (↑N) l')%I
+    iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "Hbf". set_solver.
+    rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
+    iMod (inv_alloc N _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid (↑N) l')%I
          with "[Hpbown]") as "#Hinv"; first by eauto.
     iExists l'. iIntros "!>{$Hbf}". iIntros (q'') "!#Htok".
     iApply (step_fupd_mask_mono (mgmtE ∪ ↑N) _ _ ((mgmtE ∪ ↑N) ∖ ↑N ∖ ↑lftN)).
@@ -233,8 +232,8 @@ Section types.
     iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iAssert (&{κ'}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
-      { rewrite /borrow. eauto. }
-      iMod (borrow_unnest with "LFT Hb") as "Hb". set_solver.
+      { rewrite (bor_unfold_idx κ'). eauto. }
+      iMod (bor_unnest with "LFT Hb") as "Hb". set_solver.
       iIntros "!>". iNext. iMod "Hb".
       iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr Htok]"; try done. set_solver.
       iMod ("Hclose" with "[]") as "_". eauto. by iFrame.
@@ -244,12 +243,12 @@ Section types.
   Qed.
   Next Obligation.
     intros κ0 ty κ κ' tid E E' l ?. iIntros "#LFT #Hκ #H".
-    iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⋅κ' ⊑ κ0⋅κ)%I as "#Hκ0".
-    { iApply (lft_incl_lb with "[] []").
-      - iApply lft_le_incl. by exists κ'.
+    iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0∪κ' ⊑ κ0∪κ)%I as "#Hκ0".
+    { iApply (lft_incl_glb with "[] []").
+      - iApply lft_le_incl. apply gmultiset_union_subseteq_l.
       - iApply (lft_incl_trans with "[] Hκ").
-        iApply lft_le_incl. exists κ0. apply (comm _). }
-    iExists l'. iSplit. by iApply (frac_borrow_shorten with "[]"). iIntros (q) "!#Htok".
+        iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
+    iExists l'. iSplit. by iApply (frac_bor_shorten with "[]"). iIntros (q) "!#Htok".
     iApply step_fupd_mask_mono. reflexivity. apply union_preserving_l. eassumption.
     iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]". set_solver.
     iMod ("Hvs" $! q' with "Htok") as "Hclose'".  iIntros "!>". iNext.
@@ -258,7 +257,7 @@ Section types.
   Qed.
   Next Obligation. done. Qed.
 
-  Program Definition shared_borrow (κ : lifetime) (ty : type) : type :=
+  Program Definition shared_bor (κ : lft) (ty : type) : type :=
     {| st_size := 1;
        st_own tid vl :=
          (∃ (l:loc), ⌜vl = [ #l ]⌝ ∗ ty.(ty_shr) κ tid (↑lrustN) l)%I |}.
@@ -300,7 +299,7 @@ Section types.
   Next Obligation.
     intros ty1 ty2 E N κ l tid q ??. iIntros "#LFT /=H Htok".
     rewrite split_prod_mt.
-    iMod (borrow_split with "LFT H") as "[H1 H2]". set_solver.
+    iMod (bor_sep with "LFT H") as "[H1 H2]". set_solver.
     iMod (ty1.(ty_share) _ (N .@ 1) with "LFT H1 Htok") as "[? Htok]". solve_ndisj. done.
     iMod (ty2.(ty_share) _ (N .@ 2) with "LFT H2 Htok") as "[? $]". solve_ndisj. done.
     iModIntro. iExists (↑N .@ 1). iExists (↑N .@ 2). iFrame.
@@ -396,22 +395,22 @@ Section types.
   Qed.
   Next Obligation.
     intros n tyl Hn E N κ l tid q ??. iIntros "#LFT Hown Htok". rewrite split_sum_mt.
-    iMod (borrow_exists with "LFT Hown") as (i) "Hown". set_solver.
-    iMod (borrow_split with "LFT Hown") as "[Hmt Hown]". set_solver.
+    iMod (bor_exists with "LFT Hown") as (i) "Hown". set_solver.
+    iMod (bor_sep with "LFT Hown") as "[Hmt Hown]". set_solver.
     iMod ((nth i tyl emp).(ty_share) with "LFT Hown Htok") as "[#Hshr $]"; try done.
-    iMod (borrow_fracture with "LFT [-]") as "H"; last by eauto. set_solver. iFrame.
+    iMod (bor_fracture with "LFT [-]") as "H"; last by eauto. set_solver. iFrame.
   Qed.
   Next Obligation.
     intros n tyl Hn κ κ' tid E E' l ?. iIntros "#LFT #Hord H".
     iDestruct "H" as (i) "[Hown0 Hown]". iExists i. iSplitL "Hown0".
-    by iApply (frac_borrow_shorten with "Hord").
+    by iApply (frac_bor_shorten with "Hord").
     iApply ((nth i tyl emp).(ty_shr_mono) with "LFT Hord"); last done. done.
   Qed.
   Next Obligation.
     intros n tyl Hn κ tid E F l q Hdup%Is_true_eq_true ?.
     iIntros "#LFT #H[[Htok1 Htok2] Htl]".
     setoid_rewrite split_sum_mt. iDestruct "H" as (i) "[Hshr0 Hshr]".
-    iMod (frac_borrow_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
+    iMod (frac_bor_acc with "LFT Hshr0 Htok1") as (q'1) "[Hown Hclose]". set_solver.
     iMod ((nth i tyl emp).(ty_shr_acc) with "LFT Hshr [Htok2 $Htl]")
       as (q'2) "[Hownq Hclose']"; try done.
     { edestruct nth_in_or_default as [| ->]; last done.
@@ -471,9 +470,9 @@ Hint Extern 1 (Types.LstTySize _ (_ :: _)) =>
 Import Types.
 
 Notation "∅" := emp : lrust_type_scope.
-Notation "&uniq{ κ } ty" := (uniq_borrow κ ty)
+Notation "&uniq{ κ } ty" := (uniq_bor κ ty)
   (format "&uniq{ κ } ty", at level 20, right associativity) : lrust_type_scope.
-Notation "&shr{ κ } ty" := (shared_borrow κ ty)
+Notation "&shr{ κ } ty" := (shared_bor κ ty)
   (format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
 
 Arguments product : simpl never.
diff --git a/theories/type_incl.v b/theories/typing/type_incl.v
similarity index 94%
rename from theories/type_incl.v
rename to theories/typing/type_incl.v
index 8ce12186257af5fd71507beb90230f11716a4aa8..060c52bcf09c573e1b50de35b55813966f0afa5d 100644
--- a/theories/type_incl.v
+++ b/theories/typing/type_incl.v
@@ -1,6 +1,7 @@
 From iris.base_logic Require Import big_op.
 From iris.program_logic Require Import hoare.
-From lrust Require Export type perm_incl.
+From lrust.typing Require Export type perm_incl.
+From lrust.lifetime Require Import frac_borrow.
 
 Import Types.
 
@@ -68,16 +69,17 @@ Section ty_incl.
       by iDestruct ("Hshri" $! _ _ _ with "Hshr") as "[$ _]".
   Qed.
 
-  Lemma lft_incl_ty_incl_uniq_borrow ty κ1 κ2 :
+  Lemma lft_incl_ty_incl_uniq_bor ty κ1 κ2 :
     ty_incl (κ1 ⊑ κ2) (&uniq{κ2}ty) (&uniq{κ1}ty).
   Proof.
     iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
     - iDestruct "H" as (l) "[% Hown]". subst. iExists _. iSplit. done.
-      by iApply (borrow_shorten with "Hincl").
-    - iAssert (κ1 ⋅ κ ⊑ κ2 ⋅ κ)%I as "#Hincl'".
-      { iApply (lft_incl_lb with "[] []").
-        - iApply (lft_incl_trans with "[] Hincl"). iApply lft_le_incl. by exists κ.
-        - iApply lft_le_incl. exists κ1. by apply (comm _). }
+      by iApply (bor_shorten with "Hincl").
+    - iAssert (κ1 ∪ κ ⊑ κ2 ∪ κ)%I as "#Hincl'".
+      { iApply (lft_incl_glb with "[] []").
+        - iApply (lft_incl_trans with "[] Hincl"). iApply lft_le_incl.
+            apply gmultiset_union_subseteq_l.
+        - iApply lft_le_incl. apply gmultiset_union_subseteq_r. }
       iSplitL; last done. iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'.
       iFrame. iIntros (q') "!#Htok".
       iMod (lft_incl_acc with "Hincl' Htok") as (q'') "[Htok Hclose]". set_solver.
@@ -86,7 +88,7 @@ Section ty_incl.
       by iApply (ty_shr_mono with "LFT Hincl' H").
   Qed.
 
-  Lemma lft_incl_ty_incl_shared_borrow ty κ1 κ2 :
+  Lemma lft_incl_ty_incl_shared_bor ty κ1 κ2 :
     ty_incl (κ1 ⊑ κ2) (&shr{κ2}ty) (&shr{κ1}ty).
   Proof.
     iIntros (tid) "#LFT #Hincl!>". iSplit; iIntros "!#*H".
@@ -172,15 +174,15 @@ Section ty_incl.
     apply (ty_incl_weaken _ ⊤). apply perm_incl_top.
     induction tyl1; last by apply (ty_incl_prod2 _ _ _ _ _ _).
     induction tyl2 as [|ty tyl2 IH]; simpl.
-    - iIntros (tid) "#LFT _". iMod (borrow_create with "LFT []") as "[Hbor _]".
+    - iIntros (tid) "#LFT _". iMod (bor_create with "LFT []") as "[Hbor _]".
       done. instantiate (1:=True%I). by auto. instantiate (1:=static).
-      iMod (borrow_fracture (λ _, True%I) with "LFT Hbor") as "#Hbor". done.
+      iMod (bor_fracture (λ _, True%I) with "LFT Hbor") as "#Hbor". done.
       iSplitL; iIntros "/=!>!#*H".
       + iExists [], vl. iFrame. auto.
       + iSplit; last done. iExists ∅, E. iSplit. iPureIntro; set_solver.
         rewrite shift_loc_0. iFrame. iExists []. iSplit; last auto.
         setoid_rewrite heap_mapsto_vec_nil.
-        iApply (frac_borrow_shorten with "[] Hbor"). iApply lft_incl_static.
+        iApply (frac_bor_shorten with "[] Hbor"). iApply lft_incl_static.
     - etransitivity; last apply ty_incl_prod2_assoc1.
       eapply (ty_incl_prod2 _ _ _ _ _ _). done. apply IH.
   Qed.
diff --git a/theories/typing.v b/theories/typing/typing.v
similarity index 91%
rename from theories/typing.v
rename to theories/typing/typing.v
index 4ba6d657725781a82e924c1517b27c2da6f014ae..ae5d0051f60a3c0586059a2755f8524f96639626 100644
--- a/theories/typing.v
+++ b/theories/typing/typing.v
@@ -1,7 +1,9 @@
 From iris.program_logic Require Import hoare.
 From iris.base_logic Require Import big_op.
-From lrust Require Export type perm notation memcpy.
-From lrust Require Import perm_incl proofmode.
+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.
 
 Import Types Perm.
 
@@ -213,7 +215,7 @@ Section typing.
       clear. induction ty.(ty_size). done. by apply (f_equal S).
   Qed.
 
-  Lemma consumes_copy_uniq_borrow ty κ κ' q:
+  Lemma consumes_copy_uniq_bor ty κ κ' q:
     ty.(ty_dup) →
     consumes ty (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
                 (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
@@ -222,7 +224,7 @@ Section typing.
     iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l') "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
-    iMod (borrow_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
+    iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
@@ -231,7 +233,7 @@ Section typing.
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
   Qed.
 
-  Lemma consumes_copy_shr_borrow ty κ κ' q:
+  Lemma consumes_copy_shr_bor ty κ κ' q:
     ty.(ty_dup) →
     consumes ty (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P
                 (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
@@ -262,7 +264,7 @@ Section typing.
     iMod "Hupd" as "[$ Hclose]". by iApply "Hclose".
   Qed.
 
-  Lemma typed_deref_uniq_borrow_own ty ν κ κ' q q':
+  Lemma typed_deref_uniq_bor_own ty ν κ κ' q q':
     typed_step (ν ◁ &uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
                (!ν)
                (λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
@@ -271,18 +273,20 @@ Section typing.
     iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
-    iMod (borrow_acc_strong with "LFT H↦ Htok") as "[H↦ Hclose']". done.
+    iMod (bor_acc_strong with "LFT H↦ Htok") as (κ0) "(#Hκκ0 & 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 (borrow_split with "LFT Hbor") as "[_ Hbor]". done.
-      iMod (borrow_split with "LFT Hbor") as "[_ Hbor]". done.
-      iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
-    - iIntros "{$H↦ $H† $Hown}!>_(?&?&?)!>". iNext. iExists _.
+    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 _.
+      iIntros "!>". iSplit. done. iApply (bor_shorten with "Hκκ0 Hbor").
+    - iFrame "H↦ H† Hown".
+    - iIntros "!>(?&?&?)_!>". iNext. iExists _.
       rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
   Qed.
 
-  Lemma typed_deref_shr_borrow_own ty ν κ κ' q q':
+  Lemma typed_deref_shr_bor_own ty ν κ κ' q q':
     typed_step (ν ◁ &shr{κ} own q' ty ∗ κ' ⊑ κ ∗ q.[κ'])
                (!ν)
                (λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ q.[κ'])%P.
@@ -292,7 +296,7 @@ Section typing.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq #H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[[Htok1 Htok2] Hclose]". done.
     iDestruct "H↦" as (vl) "[H↦b Hown]".
-    iMod (frac_borrow_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
+    iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     iSpecialize ("Hown" $! _ with "Htok2").
     iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
     - iApply (wp_frame_step_l _ (↑heapN) _ (λ v, l ↦{q'''} v ∗ ⌜v = #vl⌝)%I); try done.
@@ -305,7 +309,7 @@ Section typing.
       iFrame "#". iExists _. eauto.
   Qed.
 
-  Lemma typed_deref_uniq_borrow_borrow ty ν κ κ' κ'' q:
+  Lemma typed_deref_uniq_bor_bor ty ν κ κ' κ'' q:
     typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
                (!ν)
                (λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
@@ -314,25 +318,25 @@ Section typing.
     iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑1 Htok") as (q'') "[Htok Hclose]". done.
-    iMod (borrow_exists with "LFT H↦") as (vl) "Hbor". done.
-    iMod (borrow_split with "LFT Hbor") as "[H↦ Hbor]". done.
-    iMod (borrow_exists with "LFT Hbor") as (l') "Hbor". done.
-    iMod (borrow_split with "LFT Hbor") as "[Heq Hbor]". done.
-    iMod (borrow_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
-    iMod (borrow_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
+    iMod (bor_exists with "LFT H↦") as (vl) "Hbor". done.
+    iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
+    iMod (bor_exists with "LFT Hbor") as (l') "Hbor". done.
+    iMod (bor_sep with "LFT Hbor") as "[Heq Hbor]". done.
+    iMod (bor_persistent with "LFT Heq Htok") as "[>% Htok]". done. subst.
+    iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
     rewrite heap_mapsto_vec_singleton.
     iApply (wp_strong_mono ⊤ ⊤ _ (λ v, _ ∗ ⌜v = #l'⌝ ∗ l ↦#l')%I). done.
     iSplitR "Hbor H↦"; last first.
     - iApply (wp_frame_step_l _ (⊤ ∖ ↑lftN) with "[-]"); try done; last first.
-      iSplitL "Hbor". by iApply (borrow_unnest with "LFT Hbor"). wp_read. auto.
+      iSplitL "Hbor". by iApply (bor_unnest with "LFT Hbor"). wp_read. auto.
     - iIntros (v) "(Hbor & % & H↦)". subst.
       iMod ("Hclose'" with "[$H↦]") as "[H↦ Htok]".
       iMod ("Hclose" with "Htok") as "$". iFrame "#".
-      iExists _. iSplitR. done. iApply (borrow_shorten with "[] Hbor").
-      iApply (lft_incl_lb with "H⊑2"). iApply lft_incl_refl.
+      iExists _. iSplitR. done. iApply (bor_shorten with "[] Hbor").
+      iApply (lft_incl_glb with "H⊑2"). iApply lft_incl_refl.
   Qed.
 
-  Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
+  Lemma typed_deref_shr_bor_bor ty ν κ κ' κ'' q:
     typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ q.[κ] ∗ κ' ⊑ κ'')
                (!ν)
                (λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ q.[κ])%P.
@@ -342,9 +346,9 @@ Section typing.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq Hshr]".
     iDestruct "Heq" as %[=->]. iDestruct "Hshr" as (l') "[H↦ Hown]".
     iMod (lft_incl_acc with "H⊑1 Htok") as (q') "[[Htok1 Htok2] Hclose]". done.
-    iMod (frac_borrow_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
-    iAssert (κ' ⊑ κ'' ⋅ κ')%I as "#H⊑3".
-    { iApply (lft_incl_lb with "H⊑2 []"). iApply lft_incl_refl. }
+    iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
+    iAssert (κ' ⊑ κ'' ∪ κ')%I as "#H⊑3".
+    { iApply (lft_incl_glb with "H⊑2 []"). iApply lft_incl_refl. }
     iMod (lft_incl_acc with "H⊑3 Htok2") as (q''') "[Htok Hclose'']". done.
     iSpecialize ("Hown" $! _ with "Htok").
     iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose' Hclose''"; last first.
@@ -388,7 +392,7 @@ Section typing.
     iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & H↦)". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
-    iMod (borrow_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
+    iMod (bor_acc with "LFT H↦ Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
     iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%#". iIntros (vl') "[H↦ Hown]".
     iMod ("Hclose'" with "[H↦ Hown]") as "[Hbor Htok]". by iExists _; iFrame.