diff --git a/_CoqProject b/_CoqProject
index 0155446ad7e6ab169ef42ec2302b504a8ee3e03b..67a059fc33d5617a4f17abc3f33848c4088ae681 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,6 +6,23 @@ theories/lifetime/creation.v
 theories/lifetime/primitive.v
 theories/lifetime/todo.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..af3550b31a09c89ddf19e8fe9f3f539bdec8a6fc 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".
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 99%
rename from theories/proofmode.v
rename to theories/lang/proofmode.v
index dbd10fe695c5eca23088bfa4f57ee6822605890d..2b327fe5e2e10700b7983ced6488ac73a85caf67 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.
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/definitions.v b/theories/lifetime/definitions.v
index fb3a87dc391b164b3c7877f311fe13abc1f195eb..8441937fb2892c5c56c9d281cf57bc453efb3b12 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -37,7 +37,7 @@ 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 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.
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 251884ae9cfabd4351f397c5f1351ece233b9cc0..e326230051083dfa27cefe1903caa2e0e3a68ef7 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -34,7 +34,7 @@ Proof.
   iMod (bor_exists with "LFT H") as ([]) "H"; auto.
 Qed.
 
-Lemma bor_persistent `{!PersistentP P} E κ q :
+Lemma bor_persistent P `{!PersistentP P} E κ q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
 Proof.
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..4f0b536a07d6f6e1d5d2abdab2c0796a124c65c8 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 derived.
 
 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..15ed02de4124b1caf263e25d890bfba456afea2b 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 rebor.
 
 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 84%
rename from theories/type.v
rename to theories/typing/type.v
index 21b23768763691738926f3dee9381080c1734e70..07430ccb7d2673aaf885f1d94c9f8c752c52f90f 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 rebor.
 
 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,24 +165,24 @@ 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.
+      { rewrite bor_unfold_idx. iExists i. eauto. }
+      iMod (bor_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.
@@ -191,7 +192,7 @@ Section types.
   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 +203,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 +218,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 +234,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 +245,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 +259,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 +301,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 +397,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 +472,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..efe320a0a905433b1a97fb0faf20a68d5c496c88 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 derived 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 92%
rename from theories/typing.v
rename to theories/typing/typing.v
index 4ba6d657725781a82e924c1517b27c2da6f014ae..28e6e81c2063b27cfc0fdaee35704e62b31511b3 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 rebor.
 
 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,18 @@ 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 "[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 (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
+      iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
       iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
     - iIntros "{$H↦ $H† $Hown}!>_(?&?&?)!>". 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 +294,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 +307,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 +316,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 +344,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 +390,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.