diff --git a/_CoqProject b/_CoqProject
index 1e60dbb99b7d7a38bcd26a1d2b2258bda21349e0..24738f7ab7050d9b5ba01c23a88da58aa89bdb69 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,8 +5,8 @@ theories/lifetime/model/faking.v
 theories/lifetime/model/creation.v
 theories/lifetime/model/primitive.v
 theories/lifetime/model/accessors.v
-theories/lifetime/model/raw_reborrow.v
 theories/lifetime/model/borrow.v
+theories/lifetime/model/borrow_sep.v
 theories/lifetime/model/reborrow.v
 theories/lifetime/lifetime_sig.v
 theories/lifetime/lifetime.v
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index c832d46cd2a1d2df6154fecff0d48bfa75fbb941..e5cbde2ad42defea9c5918c0724793871cecbb84 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -1,6 +1,6 @@
 From lrust.lifetime Require Export lifetime_sig.
 From lrust.lifetime.model Require definitions primitive accessors faking borrow
-     reborrow creation.
+     borrow_sep reborrow creation.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
@@ -10,6 +10,7 @@ Module Export lifetime : lifetime_sig.
   Include primitive.
   Include borrow.
   Include faking.
+  Include borrow_sep.
   Include reborrow.
   Include accessors.
   Include creation.
@@ -25,6 +26,17 @@ Section derived.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
+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_cons with "LFT HP") as "[[HP Hclose]|[? ?]]"; first done.
+  - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "[] HP"); auto.
+  - iRight. by iFrame.
+Qed.
+
 Lemma bor_acc_cons E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
@@ -46,6 +58,17 @@ Proof.
   iIntros "!>HP". iMod ("Hclose" with "[] HP") as "[$ $]"; auto.
 Qed.
 
+Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+Proof.
+  iIntros (?) "#LFT Hb".
+  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
+  - iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
+    iExists x. iApply ("Hclose" with "[] HΦ"). iIntros "!> ?"; eauto.
+  - iExists inhabitant. by iApply (bor_fake with "LFT").
+Qed.
+
 Lemma bor_or E κ P Q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}(P ∨ Q) ={E}=∗ (&{κ}P ∨ &{κ}Q).
@@ -78,6 +101,7 @@ Lemma later_bor_static E P :
 Proof.
   iIntros (?) "#LFT HP". iMod (bor_create with "LFT HP") as "[$ _]"; done.
 Qed.
+
 Lemma bor_static_later E P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{static} P ={E}=∗ ▷ P.
@@ -95,6 +119,34 @@ Proof.
   iModIntro. iNext. iApply ("Hclose" with "[] HP"). by iIntros "!> $".
 Qed.
 
+Lemma rebor E κ κ' P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
+Proof.
+  iIntros (?) "#LFT #Hκ'κ Hbor". rewrite [(&{κ}P)%I]bor_unfold_idx.
+  iDestruct "Hbor" as (i) "[#Hbor Hidx]".
+  iMod (bor_create _ κ' with "LFT Hidx") as "[Hidx Hinh]"; first done.
+  iMod (idx_bor_unnest with "LFT Hbor Hidx") as "Hbor'"; first done.
+  iDestruct (bor_shorten with "[] Hbor'") as "$".
+  { iApply lft_incl_glb. done. iApply lft_incl_refl. }
+  iIntros "!> H†". iMod ("Hinh" with "H†") as ">Hidx". auto with iFrame.
+Qed.
+
+Lemma bor_unnest E κ κ' P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ'} &{κ} P ={E}▷=∗ &{κ ⊓ κ'} P.
+Proof.
+  iIntros (?) "#LFT Hbor".
+  iMod (bor_acc_atomic_cons with "LFT Hbor") as
+      "[[Hbor Hclose]|[H† Hclose]]"; first done.
+  - rewrite ->bor_unfold_idx. iDestruct "Hbor" as (i) "[#Hidx Hbor]".
+    iMod ("Hclose" with "[] Hbor") as "Hbor".
+    { iIntros "!> H". rewrite bor_unfold_idx. auto with iFrame. }
+    iIntros "!>"; iNext. by iApply (idx_bor_unnest with "LFT Hidx Hbor").
+  - iMod "Hclose" as "_". iApply (bor_fake with "LFT"); first done.
+    rewrite -lft_dead_or. auto.
+Qed.
+
 Lemma bor_persistent P `{!PersistentP P} E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P ={E}=∗ ▷ P ∨ [†κ].
@@ -129,5 +181,4 @@ Proof.
   - iApply lft_incl_trans; last iApply IH. (* FIXME: Why does "done" not do this? Looks like "assumption" to me. *)
     iApply lft_intersect_incl_r.
 Qed.
-  
 End derived.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 446e1598c5aea6739ca78feacb4ccc063f523353..22f12192c9d38d48c101d9ca345effa079700d76 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -54,6 +54,9 @@ Module Type lifetime_sig.
   Context `{invG, lftG Σ}.
 
   (** Instances *)
+  Global Declare Instance lft_inhabited : Inhabited lft.
+  Global Declare Instance bor_idx_inhabited : Inhabited bor_idx.
+
   Global Declare Instance lft_intersect_comm : Comm eq lft_intersect.
   Global Declare Instance lft_intersect_assoc : Assoc eq lft_intersect.
   Global Declare Instance lft_intersect_inj_1 κ : Inj eq eq (lft_intersect κ).
@@ -109,16 +112,14 @@ Module Type lifetime_sig.
   Parameter bor_combine : ∀ E κ P Q,
     ↑lftN ⊆ E → lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
 
-  Parameter rebor : ∀ E κ κ' P,
-    ↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
-  Parameter bor_unnest : ∀ E κ κ' P,
-    ↑lftN ⊆ E → lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ⊓ κ'} P.
-
   Parameter bor_unfold_idx : ∀ κ P, &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
 
   Parameter idx_bor_shorten : ∀ κ κ' i P, κ ⊑ κ' -∗ &{κ',i} P -∗ &{κ,i} P.
   Parameter idx_bor_iff : ∀ κ i P P', ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
 
+  Parameter idx_bor_unnest : ∀ E κ κ' i P,
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ,i} P -∗ &{κ'} idx_bor_own 1 i ={E}=∗ &{κ ⊓ κ'} P.
+
   Parameter idx_bor_acc : ∀ E q κ i P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗
       ▷ P ∗ (▷ P ={E}=∗ idx_bor_own 1 i ∗ q.[κ]).
@@ -154,15 +155,10 @@ Module Type lifetime_sig.
                  lft_tok q' κ' ∗ (lft_tok q' κ' ={↑lftN}=∗ lft_tok q κ)) ∗
         (lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
   (* Same for some of the derived lemmas. *)
-  Parameter bor_exists : ∀ {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ,
-    ↑lftN ⊆ E → lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
   Parameter bor_acc_atomic_cons : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
       (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
       ([†κ] ∗ |={E∖↑lftN,E}=> True).
-  Parameter bor_acc_atomic : ∀ E κ P,
-    ↑lftN ⊆ E → lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
-       (▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ &{κ}P)) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True).
 
   End properties.
 
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 7362f5e8079b1db6729750f1936bbbe01f66be3b..760216d85c715ef67923ba1923c1127aed066e23 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -281,15 +281,4 @@ Proof.
     + iApply (bor_shorten with "Hκκ' Hb").
   - iRight. by iFrame.
 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_cons with "LFT HP") as "[[HP Hclose]|[? ?]]"; first done.
-  - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "[] HP"); auto.
-  - iRight. by iFrame.
-Qed.
 End accessors.
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 94d545f501c7ae9e74c56a166a88071923895695..cbc8e364b3a12d6e2dd047b013638345376de18e 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -1,5 +1,5 @@
 From lrust.lifetime Require Export primitive.
-From lrust.lifetime Require Export faking raw_reborrow.
+From lrust.lifetime Require Export faking.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
@@ -10,9 +10,9 @@ Section borrow.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-Lemma bor_create E κ P :
+Lemma raw_bor_create E κ P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
+  lft_ctx -∗ ▷ P ={E}=∗ raw_bor κ P ∗ ([†κ] ={E}=∗ ▷ P).
 Proof.
   iIntros (HE) "#LFT HP". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   iMod (ilft_create _ _ κ with "HA HI Hinv") as (A' I') "(Hκ & HA & HI & Hinv)".
@@ -43,8 +43,7 @@ Proof.
       simpl. 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. iFrame.
+    + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame.
       iExists P. rewrite -uPred.iff_refl. auto.
     + clear -HE. iIntros "!> H†".
       iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
@@ -63,137 +62,16 @@ Proof.
   - 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.
+    unfold bor. iFrame. iApply "Hclose". iExists _, _. iFrame. rewrite big_sepS_later.
+    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) "#LFT Hbor". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  rewrite {1}/bor. iDestruct "Hbor" as (κ') "[#Hκκ' Hbor]".
-  rewrite /raw_bor /idx_bor_own. iDestruct "Hbor" as (s) "[Hbor Hslice]".
-  iDestruct "Hslice" as (P') "[#HPP' 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_iff _ _ true with "HPP' Hslice Hbox")
-      as (s' Pb') "(% & #HPbPb' & Hslice & Hbox)"; first solve_ndisj.
-    { by rewrite lookup_fmap EQB. }
-    iAssert (▷ lft_vs κ' Pb' Pi)%I with "[Hvs]" as "Hvs".
-    { iNext. iApply (lft_vs_cons false with "[] Hvs"). iIntros "[$ ?]!>".
-      by iApply "HPbPb'". }
-    iMod (slice_split _ _ true with "Hslice Hbox")
-      as (γ1 γ2) "(Hγ1 & Hγ2 & % & Hs1 & Hs2 & Hbox)"; first solve_ndisj.
-    { by rewrite lookup_insert. }
-    rewrite delete_insert //. iDestruct "Hγ1" as %Hγ1. iDestruct "Hγ2" as %Hγ2.
-    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, to_agree 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, to_agree 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. iExists P. rewrite -uPred.iff_refl. auto. }
-    iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
-    { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2.
-      iFrame. iExists Q. rewrite -uPred.iff_refl. auto. }
-    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 :
+Lemma bor_create E κ P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
+  lft_ctx -∗ ▷ P ={E}=∗ &{κ}P ∗ ([†κ] ={E}=∗ ▷ P).
 Proof.
-  iIntros (?) "#LFT 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 "LFT Hbor1") as "[Hbor1 _]".
-    done. by apply gmultiset_union_subseteq_l.
-  iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT 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 "Hslice1" as (P') "[#HPP' Hslice1]".
-  iDestruct "Hslice2" as (Q') "[#HQQ' 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.
-      by intros [[]]. }
-    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, to_agree 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. iExists _. iFrame. iNext. iAlways.
-      by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
-    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) /=. iNext. simpl.
-      rewrite [([∗ map] _ ∈ delete _ _, _)%I](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").
+  iIntros (?) "#LFT HP". iMod (raw_bor_create with "LFT HP") as "[HP $]"; [done|].
+  rewrite /bor. iExists _. iFrame. iApply lft_incl_refl.
 Qed.
 End borrow.
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
new file mode 100644
index 0000000000000000000000000000000000000000..af31754c9b5ed3514e1ebf8194da4b0e0aa8e73d
--- /dev/null
+++ b/theories/lifetime/model/borrow_sep.v
@@ -0,0 +1,141 @@
+From lrust.lifetime Require Export primitive.
+From lrust.lifetime Require Export faking reborrow.
+From iris.algebra Require Import csum auth frac gmap agree.
+From iris.base_logic Require Import big_op.
+From iris.base_logic.lib Require Import boxes.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+Section borrow.
+Context `{invG Σ, lftG Σ}.
+Implicit Types κ : lft.
+
+Lemma bor_sep E κ P Q :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
+Proof.
+  iIntros (HE) "#LFT Hbor". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  rewrite {1}/bor. iDestruct "Hbor" as (κ') "[#Hκκ' Hbor]".
+  rewrite /raw_bor /idx_bor_own. iDestruct "Hbor" as (s) "[Hbor Hslice]".
+  iDestruct "Hslice" as (P') "[#HPP' 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_iff _ _ true with "HPP' Hslice Hbox")
+      as (s' Pb') "(% & #HPbPb' & Hslice & Hbox)"; first solve_ndisj.
+    { by rewrite lookup_fmap EQB. }
+    iAssert (▷ lft_vs κ' Pb' Pi)%I with "[Hvs]" as "Hvs".
+    { iNext. iApply (lft_vs_cons false with "[] Hvs"). iIntros "[$ ?]!>".
+      by iApply "HPbPb'". }
+    iMod (slice_split _ _ true with "Hslice Hbox")
+      as (γ1 γ2) "(Hγ1 & Hγ2 & % & Hs1 & Hs2 & Hbox)"; first solve_ndisj.
+    { by rewrite lookup_insert. }
+    rewrite delete_insert //. iDestruct "Hγ1" as %Hγ1. iDestruct "Hγ2" as %Hγ2.
+    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, to_agree 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, to_agree 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. iExists P. rewrite -uPred.iff_refl. auto. }
+    iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
+    { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2.
+      iFrame. iExists Q. rewrite -uPred.iff_refl. auto. }
+    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 (?) "#LFT 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 "LFT Hbor1") as "[Hbor1 _]".
+    done. by apply gmultiset_union_subseteq_l.
+  iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT 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 "Hslice1" as (P') "[#HPP' Hslice1]".
+  iDestruct "Hslice2" as (Q') "[#HQQ' 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.
+      by intros [[]]. }
+    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, to_agree 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. iExists _. iFrame. iNext. iAlways.
+      by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
+    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) /=. iNext. simpl.
+      rewrite [([∗ map] _ ∈ delete _ _, _)%I](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.
\ No newline at end of file
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 449092542343f50435b94333b2435a9389af3d65..cecfbf4cef38c0dca9b739ace9a403efc60e1510 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -262,6 +262,8 @@ Proof.
 Qed.
 
 (** Basic rules about lifetimes  *)
+Instance lft_inhabited : Inhabited lft := _.
+Instance bor_idx_inhabited : Inhabited bor_idx := _.
 Instance lft_intersect_comm : Comm eq lft_intersect := _.
 Instance lft_intersect_assoc : Assoc eq lft_intersect := _.
 Instance lft_intersect_inj_1 κ : Inj eq eq (lft_intersect κ) := _.
diff --git a/theories/lifetime/model/raw_reborrow.v b/theories/lifetime/model/raw_reborrow.v
deleted file mode 100644
index 78be6b25c17007e9e5e67a38f228fba43593660b..0000000000000000000000000000000000000000
--- a/theories/lifetime/model/raw_reborrow.v
+++ /dev/null
@@ -1,200 +0,0 @@
-From lrust.lifetime Require Export primitive.
-From lrust.lifetime Require Import faking.
-From iris.algebra Require Import csum auth frac gmap agree gset.
-From iris.base_logic Require Import big_op.
-From iris.base_logic.lib Require Import boxes.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
-
-Section rebor.
-Context `{invG Σ, lftG Σ}.
-Implicit Types κ : lft.
-
-(* Notice that taking lft_inv for both κ and κ' already implies
-   κ ≠ κ'.  Still, it is probably more instructing to require
-   κ ⊂ κ' in this lemma (as opposed to just κ ⊆ κ'), and it
-   should not increase the burden on the user. *)
-Lemma raw_bor_unnest E q A I Pb Pi P κ i κ' :
-  ↑borN ⊆ E →
-  let Iinv := (own_ilft_auth I ∗ ▷?q lft_inv A κ)%I in
-  κ ⊂ κ' →
-  lft_alive_in A κ' →
-  Iinv -∗ idx_bor_own 1 (κ, i) -∗ slice borN i P -∗ ▷?q lft_bor_alive κ' Pb -∗
-  ▷?q lft_vs κ' (idx_bor_own 1 (κ, i) ∗ Pb) Pi ={E}=∗ ∃ Pb',
-    Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs κ' Pb' Pi.
-Proof.
-  iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hκ) Hi #Hislice Hκalive' Hvs".
-  rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hn● Hvs]".
-  iMod (own_cnt_update with "Hn●") as "[Hn● H◯]".
-  { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
-  rewrite {1}/raw_bor /idx_bor_own /=.
-  iDestruct (own_bor_auth with "HI Hi") as %?.
-  assert (κ ⊆ κ') by (by apply strict_include).
-  iDestruct (lft_inv_alive_in with "Hκ") as "Hκ";
-    first by eauto using lft_alive_in_subseteq.
-  rewrite lft_inv_alive_unfold;
-    iDestruct "Hκ" as (Pb' Pi') "(Hκalive&Hvs'&Hinh')".
-  rewrite {2}/lft_bor_alive; iDestruct "Hκalive" as (B) "(Hbox & >HB● & HB)".
-  iDestruct (own_bor_valid_2 with "HB● Hi")
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
-  { by rewrite lookup_fmap HB. }
-  iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
-  { eapply auth_update, singleton_local_update; last eapply
-     (exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
-    rewrite /to_borUR lookup_fmap. by rewrite HB. }
-  iAssert (▷?q lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
-  { 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 HB●".
-    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; auto. }
-  clear B HB Pb' Pi'.
-  rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >HB● & HB)".
-  iMod (slice_insert_full 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 "HB●") as "[HB● Hj]".
-  { apply auth_update_alloc,
-     (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
-    rewrite /to_borUR lookup_fmap. by rewrite HBj. }
-  iModIntro. iExists (P ∗ Pb)%  I. rewrite /Iinv. iFrame "HI". iFrame.
-  iSplitL "Hj".
-  { rewrite /raw_bor /idx_bor_own. iExists j. iFrame. iExists P.
-    rewrite -uPred.iff_refl. auto. }
-  iSplitL "Hbox HB● HB".
-  { 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 "Hn●".
-  iIntros (I) "Hinv [HP HPb] #Hκ†".
-  rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
-  iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
-  iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
-  rewrite lft_inv_alive_unfold.
-  iDestruct ("Hκalive" with "[%]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)"; first done.
-  rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
-  iDestruct (own_bor_valid_2 with "HB● Hi") 
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
-  { eapply auth_update, singleton_local_update,
-     (exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
-    rewrite /to_borUR lookup_fmap. by rewrite HB. }
-  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 "[Hcnt HB]"; first done.
-  rewrite /=. iDestruct "Hcnt" as "[% H1â—¯]".
-  iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
-                         [$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
-  { rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
-    iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); 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 /=. auto. }
-  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
-  by iFrame.
-Qed.
-
-Lemma raw_bor_unnest' E q A I Pb Pi P κ κ' :
-  ↑borN ⊆ E →
-  let Iinv := (
-    own_ilft_auth I ∗
-    ▷?q [∗ set] κ ∈ dom _ I ∖ {[κ']}, lft_inv A κ)%I in
-  κ ⊆ κ' →
-  lft_alive_in A κ' →
-  Iinv -∗ raw_bor κ P -∗ ▷?q lft_bor_alive κ' Pb -∗
-  ▷?q lft_vs κ' (raw_bor κ P ∗ Pb) Pi ={E}=∗ ∃ Pb',
-    Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs κ' Pb' Pi.
-Proof.
-  iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hinv) Hraw Hκalive' Hvs".
-  destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iModIntro. iExists Pb. rewrite /Iinv. iFrame "HI Hinv Hκalive' Hraw".
-    iApply (lft_vs_cons with "[]"); last done.
-    iIntros "(Hdead & HPb)".
-    iMod (raw_bor_fake _ false _ P with "Hdead") as "[Hdead Hraw]"; first solve_ndisj.
-    by iFrame. }
-  assert (κ ⊂ κ') by (by apply strict_spec_alt).
-  iDestruct (raw_bor_inI with "HI Hraw") as %HI.
-  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose]".
-  { rewrite elem_of_difference elem_of_dom not_elem_of_singleton. done. }
-  rewrite {1}/raw_bor. iDestruct "Hraw" as (i) "[Hi #Hislice]".
-  iDestruct "Hislice" as (P') "[#HPP' Hislice]".
-  iMod (raw_bor_unnest with "[$HI $Hinv] Hi Hislice Hκalive' [Hvs]")
-    as (Pb') "([HI Hκ] & ? & ? & ?)"; [done..| |].
-  { iApply (lft_vs_cons with "[]"); last done.
-    iIntros "[$ [>? $]]". iModIntro. iNext. rewrite /raw_bor.
-    iExists i. iFrame. iExists _. iFrame "#". }
-  iExists Pb'. iModIntro. iFrame. iSplitL "Hclose Hκ". by iApply "Hclose".
-  by iApply (raw_bor_iff with "HPP'").
-Qed.
-
-Lemma raw_rebor E κ κ' P :
-  ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx -∗ raw_bor κ P ={E}=∗
-    raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
-Proof.
-  rewrite /lft_ctx. iIntros (??) "#LFT Hκ".
-  destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iFrame. iIntros "!> #Hκ†". by iApply (raw_bor_fake' with "LFT Hκ†"). }
-  assert (κ ⊂ κ') by (by apply strict_spec_alt).
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iMod (ilft_create _ _ κ' with "HA HI Hinv") as (A' I') "(% & HA & HI & Hinv)".
-  clear A I; rename A' into A; rename I' into I.
-  iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
-    first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[? >%]|[Hdead >%]]"; last first.
-  { rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & >H● & Hinh)".
-    iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead $]"; first solve_ndisj.
-    iMod ("Hclose" with "[-Hκ]") as "_"; last auto.
-    iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
-    iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom.
-    iFrame "Hinv". rewrite /lft_inv /lft_inv_dead. iRight.
-    iSplit; last done. iExists Pi. by iFrame. }
-  rewrite lft_inv_alive_unfold; iDestruct "Hκinv'" as (Pb Pi) "(Hbor & Hvs & Hinh)".
-  rewrite {1}/raw_bor. iDestruct "Hκ" as (i) "[Hi #Hislice]".
-  iDestruct "Hislice" as (P') "[#HPP' Hislice]".
-  iMod (lft_inh_extend _ _ (idx_bor_own 1 (κ, i)) with "Hinh")
-    as "(Hinh & HIlookup & Hinh_close)"; first solve_ndisj.
-  iDestruct (own_bor_auth with "HI [Hi]") as %?.
-  { by rewrite /idx_bor_own. }
-  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hκ Hκclose]".
-  { by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
-  iMod (raw_bor_unnest _ true _ _ _ (idx_bor_own 1 (κ, i) ∗ Pi)%I
-    with "[$HI $Hκ] Hi Hislice Hbor [Hvs]")
-    as (Pb') "([HI Hκ] & HP' & Halive & Hvs)"; [solve_ndisj|done|done|..].
-  { iNext. by iApply lft_vs_frame. }
-  iDestruct (raw_bor_iff with "HPP' HP'") as "$".
-  iDestruct ("Hκclose" with "Hκ") as "Hinv".
-  iMod ("Hclose" with "[HA HI Hinv Halive Hinh Hvs]") as "_".
-  { iNext. rewrite {2}/lfts_inv. iExists A, I. iFrame "HA HI".
-    iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
-    rewrite /lft_inv. iLeft. iSplit; last done.
-    rewrite lft_inv_alive_unfold. iExists Pb', (idx_bor_own 1 (κ, i) ∗ Pi)%I.
-    iFrame. }
-  clear dependent A I Pb Pb' Pi. iModIntro. iIntros "H†".
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iDestruct ("HIlookup" with "HI") as %Hκ'.
-  iDestruct (big_sepS_delete _ _ κ' with "Hinv") as "[Hκinv' Hinv]";
-    first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hκinv'" as "[[Halive >%]|[Hdead >%]]".
-  - (* the same proof is in bor_fake and bor_create *)
-    rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
-    iDestruct (own_alft_auth_agree A Λ false with "HA H†") as %EQAΛ.
-    unfold lft_alive_in in *. naive_solver.
-  - rewrite /lft_inv_dead; iDestruct "Hdead" as (Pi) "(Hdead & Hcnt & Hinh)".
-    iMod ("Hinh_close" $! Pi with "Hinh") as (Pi') "(Heq & >Hbor & Hinh)".
-    iMod ("Hclose" with "[HA HI Hinv Hdead Hinh Hcnt]") as "_".
-    { iNext. rewrite /lfts_inv. iExists A, I. iFrame "HA HI".
-      iApply (big_sepS_delete _ _ κ'); first by apply elem_of_dom. iFrame "Hinv".
-      rewrite /lft_inv /lft_inv_dead. iRight. iSplit; last done.
-      iExists Pi'. iFrame. }
-    iModIntro. rewrite /raw_bor. iExists i. iFrame. iExists _. auto.
-Qed.
-End rebor.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 17957f5ebdb2fafe6d89755f0a2d6736447c4bd7..80365b67a573d828c159128afdf8dadded3f5873 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -1,5 +1,4 @@
-From lrust.lifetime Require Export borrow.
-From lrust.lifetime Require Import raw_reborrow accessors.
+From lrust.lifetime Require Import borrow accessors.
 From iris.algebra Require Import csum auth frac gmap agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
@@ -10,96 +9,183 @@ Section reborrow.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-(* This lemma has no good place... and reborrowing is where we need it inside the model. *)
-Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+(* Notice that taking lft_inv for both κ and κ' already implies
+   κ ≠ κ'.  Still, it is probably more instructing to require
+   κ ⊂ κ' in this lemma (as opposed to just κ ⊆ κ'), and it
+   should not increase the burden on the user. *)
+Lemma raw_bor_unnest E q A I Pb Pi P κ i κ' :
+  ↑borN ⊆ E →
+  let Iinv := (own_ilft_auth I ∗ ▷?q lft_inv A κ)%I in
+  κ ⊂ κ' →
+  lft_alive_in A κ' →
+  Iinv -∗ idx_bor_own 1 (κ, i) -∗ slice borN i P -∗ ▷?q lft_bor_alive κ' Pb -∗
+  ▷?q lft_vs κ' (idx_bor_own 1 (κ, i) ∗ Pb) Pi ={E}=∗ ∃ Pb',
+    Iinv ∗ raw_bor κ' P ∗ ▷?q lft_bor_alive κ' Pb' ∗ ▷?q lft_vs κ' Pb' Pi.
 Proof.
-  iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
-  - iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
-    iExists x. iApply ("Hclose" with "[] HΦ"). iIntros "!> ?"; eauto.
-  - iExists inhabitant. by iApply (bor_fake with "LFT").
+  iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hκ) Hi #Hislice Hκalive' Hvs".
+  rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hn● Hvs]".
+  iMod (own_cnt_update with "Hn●") as "[Hn● H◯]".
+  { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
+  rewrite {1}/raw_bor /idx_bor_own /=.
+  iDestruct (own_bor_auth with "HI Hi") as %?.
+  assert (κ ⊆ κ') by (by apply strict_include).
+  iDestruct (lft_inv_alive_in with "Hκ") as "Hκ";
+    first by eauto using lft_alive_in_subseteq.
+  rewrite lft_inv_alive_unfold;
+    iDestruct "Hκ" as (Pb' Pi') "(Hκalive&Hvs'&Hinh')".
+  rewrite {2}/lft_bor_alive; iDestruct "Hκalive" as (B) "(Hbox & >HB● & HB)".
+  iDestruct (own_bor_valid_2 with "HB● Hi")
+    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
+  iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
+  { by rewrite lookup_fmap HB. }
+  iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
+  { eapply auth_update, singleton_local_update; last eapply
+     (exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
+    rewrite /to_borUR lookup_fmap. by rewrite HB. }
+  iAssert (▷?q lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
+  { 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 HB●".
+    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; auto. }
+  clear B HB Pb' Pi'.
+  rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >HB● & HB)".
+  iMod (slice_insert_full 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 "HB●") as "[HB● Hj]".
+  { apply auth_update_alloc,
+     (alloc_singleton_local_update _ j (1%Qp, to_agree Bor_in)); last done.
+    rewrite /to_borUR lookup_fmap. by rewrite HBj. }
+  iModIntro. iExists (P ∗ Pb)%  I. rewrite /Iinv. iFrame "HI". iFrame.
+  iSplitL "Hj".
+  { rewrite /raw_bor /idx_bor_own. iExists j. iFrame. iExists P.
+    rewrite -uPred.iff_refl. auto. }
+  iSplitL "Hbox HB● HB".
+  { 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 "Hn●".
+  iIntros (I) "Hinv [HP HPb] #Hκ†".
+  rewrite {1}lft_vs_inv_unfold; iDestruct "Hinv" as "(Hκdead' & HI & Hinv)".
+  iDestruct (own_bor_auth with "HI Hi") as %?%elem_of_dom.
+  iDestruct (@big_sepS_delete with "Hinv") as "[Hκalive Hinv]"; first done.
+  rewrite lft_inv_alive_unfold.
+  iDestruct ("Hκalive" with "[%]") as (Pb' Pi') "(Hκalive&Hvs'&Hinh)"; first done.
+  rewrite /lft_bor_alive; iDestruct "Hκalive" as (B') "(Hbox & HB● & HB)".
+  iDestruct (own_bor_valid_2 with "HB● Hi")
+    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
+  iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
+  { eapply auth_update, singleton_local_update,
+     (exclusive_local_update _ (1%Qp, to_agree Bor_in)); last done.
+    rewrite /to_borUR lookup_fmap. by rewrite HB. }
+  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 "[Hcnt HB]"; first done.
+  rewrite /=. iDestruct "Hcnt" as "[% H1â—¯]".
+  iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
+                         [$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
+  { rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
+    iApply (big_sepS_delete _ (dom (gset lft) I) with "[- $Hinv]"); 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 /=. auto. }
+  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
+  by iFrame.
 Qed.
 
-Lemma rebor E κ κ' P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
+Lemma raw_idx_bor_unnest E κ κ' i P :
+  ↑lftN ⊆ E → κ ⊂ κ' →
+  lft_ctx -∗ slice borN i P -∗ raw_bor κ' (idx_bor_own 1 (κ, i))
+  ={E}=∗ raw_bor κ' P.
+Proof.
+  iIntros (? Hκκ') "#LFT #Hs Hraw".
+  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  iDestruct (raw_bor_inI with "HI Hraw") as %HI'.
+  rewrite (big_sepS_delete _ _ κ') ?elem_of_dom // [_ A κ']/lft_inv.
+  iDestruct "Hinv" as "[[[Hinvκ >%]|[Hinvκ >%]] Hinv]"; last first.
+  { rewrite /lft_inv_dead. iDestruct "Hinvκ" as (Pi) "[Hbordead H]".
+    iMod (raw_bor_fake _ true with "Hbordead") as "[Hbordead $]";
+      first solve_ndisj.
+    iApply "Hclose". iExists _, _. iFrame.
+    rewrite (big_opS_delete _ (dom _ _) κ') ?elem_of_dom // /lft_inv /lft_inv_dead.
+    auto 10 with iFrame. }
+  rewrite {1}/raw_bor. iDestruct "Hraw" as (i') "[Hbor H]".
+  iDestruct "H" as (P') "[#HP' #Hs']".
+  rewrite lft_inv_alive_unfold /lft_bor_alive [in _ _ (κ', i')]/idx_bor_own.
+  iDestruct "Hinvκ" as (Pb Pi) "(Halive & Hvs & Hinh)".
+  iDestruct "Halive" as (B) "(Hbox & >H● & HB)".
+  iDestruct (own_bor_valid_2 with "H● Hbor")
+    as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
+  iMod (slice_empty _ _ true with "Hs' Hbox") as "[Hidx Hbox]".
+    solve_ndisj. by rewrite lookup_fmap EQB.
+  iAssert (▷ idx_bor_own 1 (κ, i))%I with "[Hidx]" as ">Hidx"; [by iApply "HP'"|].
+  iDestruct (raw_bor_inI _ _ P with "HI [Hidx]") as %HI;
+    first by rewrite /raw_bor; auto 10 with I.
+  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinvκ Hclose']";
+    first by rewrite elem_of_difference elem_of_dom not_elem_of_singleton;
+    eauto using strict_ne.
+  iMod (slice_delete_empty with "Hs' Hbox") as (Pb') "[#HeqPb' Hbox]";
+    [solve_ndisj|by apply lookup_insert|].
+  iMod (own_bor_update_2 with "H● Hbor") as "H●".
+  { apply auth_update_dealloc, delete_singleton_local_update. apply _. }
+  iMod (raw_bor_unnest _ true with "[$HI $Hinvκ] Hidx Hs [Hbox H● HB] [Hvs]")
+    as (Pb'') "HH"; [solve_ndisj|done|done| | |].
+  { rewrite /lft_bor_alive (big_sepM_delete _ B i') //. iDestruct "HB" as "[_ HB]".
+    iExists (delete i' B). rewrite -fmap_delete. iFrame.
+    rewrite fmap_delete -insert_delete delete_insert ?lookup_delete //=. }
+  { iNext. iApply (lft_vs_cons false with "[] Hvs"). iIntros "[$ [??]] !>". iNext.
+    iRewrite "HeqPb'". iFrame. by iApply "HP'". }
+  iDestruct "HH" as "([HI Hinvκ] & $ & Halive & Hvs)".
+  iApply "Hclose". iExists _, _. iFrame.
+  rewrite (big_opS_delete _ (dom _ _) κ') ?elem_of_dom //.
+  iDestruct ("Hclose'" with "Hinvκ") as "$".
+  rewrite /lft_inv lft_inv_alive_unfold. auto 10 with iFrame.
+Qed.
+
+Lemma raw_rebor E κ κ' P :
+  ↑lftN ⊆ E → κ ⊆ κ' →
+  lft_ctx -∗ raw_bor κ P ={E}=∗ raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
 Proof.
-  iIntros (?) "#LFT #H⊑". rewrite {1}/bor; iDestruct 1 as (κ'') "[#H⊑' Hκ'']".
-  iMod (raw_rebor _ _ (κ' ⊓ κ'') with "LFT Hκ''") as "[Hκ'' Hclose]"; first done.
-  { apply gmultiset_union_subseteq_r. }
-  iModIntro. iSplitL "Hκ''".
-  - rewrite /bor. iExists (κ' ⊓ κ''). iFrame "Hκ''".
-    iApply (lft_incl_glb with "[]"); first iApply lft_incl_refl.
-    by iApply (lft_incl_trans with "H⊑").
-  - iIntros "Hκ†". iMod ("Hclose" with "[Hκ†]") as "Hκ''".
-    { iApply lft_dead_or; auto. }
-    iModIntro. rewrite /bor. eauto.
+  iIntros (? Hκκ') "#LFT Hbor".
+  destruct (decide (κ = κ')) as [<-|Hκneq].
+  { iFrame. iIntros "!> H†". by iApply raw_bor_fake'. }
+  assert (κ ⊂ κ') by (by apply strict_spec_alt).
+  rewrite [_ κ P]/raw_bor. iDestruct "Hbor" as (s) "[Hbor Hs]".
+  iDestruct "Hs" as (P') "[#HP'P #Hs]".
+  iMod (raw_bor_create _ κ' with "LFT Hbor") as "[Hbor Hinh]"; first done.
+  iSplitR "Hinh"; first last.
+  { iIntros "!> #H†". iExists _. iMod ("Hinh" with "H†") as ">$". auto with iFrame. }
+  iApply (raw_bor_iff with "HP'P"). by iApply raw_idx_bor_unnest.
 Qed.
 
-Lemma bor_unnest E κ κ' P :
+Lemma idx_bor_unnest E κ κ' i P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ⊓ κ'} P.
+  lft_ctx -∗ &{κ,i} P -∗ &{κ'} idx_bor_own 1 i ={E}=∗ &{κ ⊓ κ'} P.
 Proof.
-  iIntros (?) "#LFT Hκ". rewrite {2}/bor.
-  iMod (bor_exists with "LFT Hκ") as (κ0) "Hκ"; first done.
-  iMod (bor_sep with "LFT Hκ") as "[Hκ⊑ Hκ]"; first done.
-  rewrite {2}/bor; iDestruct "Hκ" as (κ0') "[#Hκ'⊑ Hκ]".
-  iMod (bor_acc_atomic with "LFT Hκ⊑") as "[[#Hκ⊑ Hclose]|[#H† Hclose]]"; first done; last first.
-  { iModIntro. iNext. iMod "Hclose" as "_". iApply (bor_fake with "LFT"); first done.
-    iApply lft_dead_or. iRight. done. }
-  iMod ("Hclose" with "Hκ⊑") as "_".
-  set (κ'' := κ0 ⊓ κ0').
-  iMod (raw_rebor _ _ κ'' with "LFT Hκ") as "[Hκ _]"; first done.
-  { apply gmultiset_union_subseteq_r. }
-  iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iMod (ilft_create _ _ κ'' with "HA HI Hinv") as (A' I') "(% & HA & HI & Hinv)".
-  clear A I; rename A' into A; rename I' into I.
-  iDestruct (big_sepS_delete _ _ κ'' with "Hinv") as "[Hκ'' Hinv]";
-    first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hκ''" as "[[Hinv' >%]|[Hdead >Hdeadin]]"; last first.
-  { iDestruct "Hdeadin" as %Hdeadin. iMod (lft_dead_in_tok with "HA") as "[HA #H†]"; first done.
-    iMod ("Hclose" with "[-]") as "_".
-    { rewrite /lfts_inv. iExists A, I. iFrame "HA HI".
-      iApply (big_sepS_delete _ _ κ''); first by apply elem_of_dom.
-      iNext; iFrame "Hinv". rewrite /lft_inv. iRight. iSplit; auto. }
-    iMod (fupd_intro_mask') as "Hclose"; last iModIntro; first solve_ndisj.
-    iNext. iMod "Hclose" as "_".
-    iApply (bor_fake with "LFT [>]"); first done.
-    iApply (lft_incl_dead with "[] H†"); first done.
-    by iApply (lft_intersect_mono with "Hκ⊑"). }
-  rewrite {1}/raw_bor /idx_bor_own /=; iDestruct "Hκ" as (i) "[Hi #Hislice]".
-  iDestruct "Hislice" as (P') "[#HPP' Hislice]".
-  rewrite lft_inv_alive_unfold;
-    iDestruct "Hinv'" as (Pb Pi) "(Halive & Hvs & Hinh)".
-  rewrite /lft_bor_alive; iDestruct "Halive" as (B) "(Hbox & >HB● & HB)".
-  iDestruct (own_bor_valid_2 with "HB● Hi")
-    as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (slice_delete_full _ _ true with "Hislice Hbox")
-    as (Pb') "(HP & #EQ & Hbox)"; first solve_ndisj.
-  { by rewrite lookup_fmap HB. }
-  iDestruct ("HPP'" with "HP") as "HP".
-  iMod (own_bor_update_2 with "HB● Hi") as "HB●".
-  { apply auth_update_dealloc, delete_singleton_local_update. apply _. }
-  iMod (fupd_intro_mask') as "Hclose'"; last iModIntro; first solve_ndisj.
-  iNext. iMod "Hclose'" as "_".
-  iAssert (lft_bor_alive κ'' Pb') with "[Hbox HB● HB]" as "Halive".
-  { rewrite /lft_bor_alive. iExists (delete i B).
-    rewrite fmap_delete. iFrame "Hbox". iSplitL "HB●".
-    - rewrite /to_borUR fmap_delete. done.
-    - rewrite big_sepM_delete; last done. iDestruct "HB" as "[_ $]". }
-  iMod (raw_bor_unnest' _ false with "[$HI $Hinv] HP Halive [Hvs]") as (Pb'') "([HI Hinv] & HP & Halive & Hvs)";
-    [solve_ndisj|exact: gmultiset_union_subseteq_l|done| |].
-  { (* TODO: Use iRewrite supporting contractive rewriting. *)
-    iApply (lft_vs_cons with "[]"); last done.
-    iIntros "[$ [Hbor HPb']]". iModIntro. iNext. iRewrite "EQ". iFrame. by iApply "HPP'". }
-  iMod ("Hclose" with "[-HP]") as "_".
-  { iNext. simpl. rewrite /lfts_inv. iExists A, I. iFrame.
-    rewrite (big_sepS_delete _ (dom _ I) κ''); last by apply elem_of_dom.
-    iFrame. rewrite /lft_inv lft_inv_alive_unfold. iLeft.
-    iFrame "%". iExists Pb'', Pi. iFrame. }
-  iModIntro. rewrite /bor. iExists κ''. iFrame. subst κ''.
-  by iApply (lft_intersect_mono with "Hκ⊑").
+  iIntros (?) "#LFT #HP Hbor".
+  rewrite [(&{κ'}_)%I]/bor. iDestruct "Hbor" as (κ'0) "[#Hκ'κ'0 Hbor]".
+  destruct (decide (κ'0 = static)) as [->|Hκ'0].
+  { iMod (bor_acc_strong with "LFT [Hbor] []") as (?) "(_ & Hbor & _)";
+      [done| |iApply (lft_tok_static 1)|].
+    - rewrite /bor. iExists static. iFrame. iApply lft_incl_refl.
+    - iDestruct "Hbor" as ">Hbor".
+      iApply bor_shorten; [|by rewrite bor_unfold_idx; auto].
+      iApply lft_intersect_incl_l. }
+  rewrite /idx_bor /bor. destruct i as [κ0 i].
+  iDestruct "HP" as "[Hκκ0 HP]". iDestruct "HP" as (P') "[HPP' HP']".
+  iMod (raw_rebor _ _ (κ0 ⊓ κ'0) with "LFT Hbor") as "[Hbor _]";
+    [done|by apply gmultiset_union_subseteq_r|].
+  iMod (raw_idx_bor_unnest with "LFT HP' Hbor") as "Hbor";
+    [done|by apply gmultiset_union_subset_l|].
+  iExists _. iDestruct (raw_bor_iff with "HPP' Hbor") as "$".
+    by iApply lft_intersect_mono.
 Qed.
 End reborrow.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index bc24f8fa20a3ff3280be6d60cd7dd5296bc2cc9e..5f13cdd3a842578530eacbdc12369bbee9a57c1b 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -113,9 +113,8 @@ Section borrow.
       try by iMod (bor_persistent_tok with "LFT Hbor Htok") as "[>[] _]".
     iMod (bor_acc with "LFT H↦ Htok") as "[>H↦ Hclose']". done.
     rewrite heap_mapsto_vec_singleton.
-    iApply (wp_step_fupd  _ (⊤∖↑lftN) with "[Hbor]"); try done.
-      by iApply (bor_unnest with "LFT Hbor").
-    iApply wp_fupd. wp_read. iIntros "!> Hbor".
+    iMod (bor_unnest with "LFT Hbor") as "Hbor"; [done|].
+    iApply wp_fupd. wp_read.
     iMod ("Hclose'" with "[H↦]") as "[H↦ Htok]"; first by auto.
     iMod ("Hclose" with "Htok") as "($ & $)".
     rewrite tctx_interp_singleton tctx_hasty_val' //.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index c0c68d79f520a1c203e5f16e49d5844db9113cfb..92171003f171e4d1c9ccdb4c2cf94ef16d3b0a07 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -41,7 +41,7 @@ Section mguard.
        ty_shr κ tid l :=
          ∃ (l':loc), &frac{κ}(λ q', l ↦{q'} #l') ∗
             □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α⊓κ]
-                ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (α⊓κ) tid (shift_loc l' 1) ∗ q.[α⊓κ]
+                ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (α⊓κ) tid (shift_loc l' 1) ∗ q.[α⊓κ]
     |}%I.
   Next Obligation. by iIntros (? ty tid [|[[]|][]]) "H". Qed.
   (* This is to a large extend copy-pasted from RWLock's write guard. *)
@@ -219,9 +219,8 @@ Section code.
     iMod (bor_sep with "LFT Hprot") as "[_ Hlm]"; first done.
     iMod (bor_persistent_tok with "LFT Hβκ Hα") as "[#Hβκ Hα]"; first done.
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hclose2]"; first done.
-    wp_bind (!_)%E. iApply (wp_step_fupd with "[Hlm]");
-      [done| |by iApply (bor_unnest with "LFT Hlm")|]; first done.
-    wp_read. iIntros "Hlm !>". wp_let.
+    wp_bind (!_)%E. iMod (bor_unnest with "LFT Hlm") as "Hlm"; first done.
+    wp_read. wp_let. iMod "Hlm".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iMod ("Hclose2" with "H↦") as "[_ Hα]".
     iMod ("Hclose1" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 029ec6d55ee405418bfae618b0cbbf7c40edf832..9cc32a04a973bc905da25cde683274acdb928d55 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -33,7 +33,7 @@ Section refmut.
          ∃ (lv lrc : loc),
            &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ]
-             ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I.
+             ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I.
   Next Obligation.
     iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
   Qed.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index fa27dacf60cfe8611f6ae32fca46f453371f5ea1..c372114653cd1a2226065c0abc708940dcdca1fb 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -86,9 +86,8 @@ Section refmut_functions.
     iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hαν". iClear "H".
     rewrite heap_mapsto_vec_cons. iMod (bor_sep with "LFT H↦") as "[H↦ _]". done.
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
-    wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hb]");
-      [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
-    wp_read. iIntros "Hb !>". wp_let.
+    wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
+    wp_read. wp_let. iMod "Hb".
     iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose'" with "Hα HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lv ◁ &uniq{α}ty]
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index fcad43bace67d4bc0eb79edff7f9aec8b014f927..9ba6c32700a9205dcd8e397224e04848dadb0be8 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -29,7 +29,7 @@ Section rwlockwriteguard.
        ty_shr κ tid l :=
          ∃ (l' : loc),
            &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
-           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ] ={F, F∖↑shrN∖↑lftN}▷=∗
+           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[α ⊓ κ] ={F, F∖↑shrN}▷=∗
                ty.(ty_shr) (α ⊓ κ) tid (shift_loc l' 1) ∗ q.[α ⊓ κ] |}%I.
   Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
   Next Obligation.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 27828ee36f8e4ce5babfd7279459880f727cfa00..c19d95e4f4a874c42ce8b14124b876fb86205432 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -84,9 +84,8 @@ Section rwlockwriteguard_functions.
     iMod (bor_sep with "LFT H") as "[Hβδ _]". done.
     iMod (bor_persistent_tok with "LFT Hβδ Hα") as "[#Hβδ Hα]". done.
     iMod (bor_acc with "LFT H↦ Hα") as "[H↦ Hcloseα]". done.
-    wp_bind (!(LitV lx'))%E. iApply (wp_step_fupd with "[Hb]");
-      [done| |by iApply (bor_unnest with "LFT Hb")|]; first done.
-    wp_read. iIntros "Hb !>". wp_op. wp_let.
+    wp_bind (!(LitV lx'))%E. iMod (bor_unnest with "LFT Hb") as "Hb"; first done.
+    wp_read. wp_op. wp_let. iMod "Hb".
     iMod ("Hcloseα" with "[$H↦]") as "[_ Hα]". iMod ("Hclose" with "Hα HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _ [ x ◁ box (uninit 1); #(shift_loc l 1) ◁ &uniq{α}ty]
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 1984922bf5c7b0a890d0718a9e31db7f28233cda..5a3a55433fa462651d1216023c52d1f8482f793a 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -18,7 +18,7 @@ Section uniq_bor.
        ty_shr κ' tid l :=
          ∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
            □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ⊓κ']
-               ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ']
+               ={F, F∖↑shrN}▷=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ']
     |}%I.
   Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
@@ -35,8 +35,7 @@ Section uniq_bor.
     iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⊓κ' ⊑ κ0⊓κ)%I as "#Hκ0".
     { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
     iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
-    iIntros "!# * % Htok".
-    iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)); try solve_ndisj.
+    iIntros "!# * % Htok". iApply (step_fupd_mask_mono F _ _ (F∖↑shrN)); try solve_ndisj.
     iMod (lft_incl_acc with "Hκ0 Htok") as (q') "[Htok Hclose]"; first solve_ndisj.
     iMod ("Hvs" with "[%] Htok") as "Hvs'"; first solve_ndisj. iModIntro. iNext.
     iMod "Hvs'" as "[#Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 784d9ad5a3210aa775a11d76c960e61b327b6ff8..fec9517556eb9deb80d3bf19fc0573801bd822f8 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -12,9 +12,12 @@ Section util.
      TODO: Figure out a nice way to generalize that; the two proofs below are too
      similar. *)
 
-  (* This is somewhat the general pattern here... but it doesn't seem easy to make
-     this usable in Coq, with the arbitrary quantifiers and things.  Also, it actually works
-     not just for borrows but for anything that you can split into a timeless and a persistent part.
+  (* This is somewhat the general pattern here... but it doesn't seem
+     easy to make this usable in Coq, with the arbitrary quantifiers
+     and things.  Also, it actually works not just for borrows but for
+     anything that you can split into a timeless and a persistent
+     part.
+
   Lemma delay_borrow_step :
     lfeE ⊆ N → (∀ x, PersistentP (Post x)) →
     lft_ctx -∗ &{κ} P -∗
@@ -32,7 +35,8 @@ Section util.
     iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
     iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ tid l)%I
           with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
+    iIntros "!> !# * % Htok".
+    iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iMod (bor_later_tok with "LFT [Hbtok] Htok") as "Hdelay"; first solve_ndisj.
       { rewrite bor_unfold_idx. eauto. }
@@ -47,13 +51,14 @@ Section util.
     lftE ⊆ N →
     lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'} &{κ} l ↦∗: ty_own ty tid ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
-       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN ∖ ↑lftN}▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
+       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
   Proof.
     iIntros (?) "#LFT #Hincl Hbor". rewrite bor_unfold_idx.
     iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
     iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ'' tid l)%I
           with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
+    iIntros "!> !# * % Htok".
+    iMod (inv_open with "Hinv") as "[INV Hclose]"; first solve_ndisj.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
     - iMod (bor_unnest with "LFT [Hbtok]") as "Hb"; first solve_ndisj.
       { iApply bor_unfold_idx. eauto. }