diff --git a/_CoqProject b/_CoqProject
index 889f911bd70797457944a1518e267acb035f1b29..c0786c8b8cdde04bce38d56d266518dcef1864f2 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,7 @@
 -Q theories lrust
 theories/lifetime/definitions.v
 theories/lifetime/derived.v
+theories/lifetime/faking.v
 theories/lifetime/creation.v
 theories/lifetime/primitive.v
 theories/lifetime/accessors.v
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index 04c1c297783d9388089c9e7fc51669659ede0914..3f036e8cb2e2a1768af5bf1400428f17d38143bb 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -1,5 +1,5 @@
-From lrust.lifetime Require Export primitive creation.
-From lrust.lifetime Require Export raw_reborrow.
+From lrust.lifetime Require Export primitive.
+From lrust.lifetime Require Export faking raw_reborrow.
 From iris.algebra Require Import csum auth frac gmap dec_agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
@@ -13,7 +13,7 @@ Lemma bor_create E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
 Proof.
-  iIntros (HE) "#Hmgmt HP". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  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)".
   iDestruct "Hκ" as %Hκ. iDestruct (@big_sepS_later with "Hinv") as "Hinv".
   iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose']".
@@ -22,7 +22,8 @@ Proof.
   - rewrite {1}lft_inv_alive_unfold;
       iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
     rewrite /lft_bor_alive; iDestruct "Halive" as (B) "(HboxB & >HownB & HB)".
-    iMod (lft_inh_acc _ _ P with "Hinh") as "[Hinh Hinh_close]"; first solve_ndisj.
+    iMod (lft_inh_extend _ _ P with "Hinh")
+      as "(Hinh & HIlookup & Hinh_close)"; first solve_ndisj.
     iMod (slice_insert_full _ _ true with "HP HboxB")
       as (γB) "(HBlookup & HsliceB & HboxB)"; first by solve_ndisj.
     rewrite lookup_fmap. iDestruct "HBlookup" as %HBlookup.
@@ -45,9 +46,7 @@ Proof.
       iModIntro. iSplit; first by iApply lft_incl_refl. iExists γB. by iFrame.
     + clear -HE. iIntros "!> H†".
       iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-      iAssert ⌜ is_Some (I !! κ) ⌝%I with "[#]" as %Hκ.
-      { iDestruct "Hinh_close" as "[H _]". by iApply "H". }
-      iDestruct "Hinh_close" as "[_ Hinh_close]".
+      iDestruct ("HIlookup" with "* HI") as %Hκ.
       iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose']".
       { by apply elem_of_dom. }
       rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
@@ -71,9 +70,9 @@ Lemma bor_sep E κ P Q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
 Proof.
-  iIntros (HE) "#Hmgmt HP". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  rewrite {1}/bor /raw_bor /idx_bor_own.
-  iDestruct "HP" as (κ') "[#Hκκ' Htmp]". iDestruct "Htmp" as (s) "[Hbor Hslice]".
+  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 (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.
@@ -123,11 +122,11 @@ Lemma bor_combine E κ P Q :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
 Proof.
-  iIntros (?) "#Hmgmt HP HQ". rewrite {1 2}/bor.
+  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 "Hmgmt Hbor1") as "[Hbor1 _]".
+  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "LFT Hbor1") as "[Hbor1 _]".
     done. by apply gmultiset_union_subseteq_l.
-  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor2") as "[Hbor2 _]".
+  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]".
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index d341c5260c6a4b001ae477e63e3389266870c2c6..b48c4cc52fb5a3ae3fd49046cf8d93607c036e77 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -1,124 +1,14 @@
 From lrust.lifetime Require Export primitive.
+From lrust.lifetime Require Import faking.
 From iris.algebra Require Import csum auth frac gmap dec_agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
 From iris.proofmode Require Import tactics.
-(* TODO: move lft_inv_alive_acc, ilft_create and bor_fake to another file. The
-files raw_reborrow, borrow and derived solely depend on this file because of
-the aforementioned lemmas. *)
 
 Section creation.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-Lemma lft_inv_alive_acc (KI K : gset lft) κ :
-  (∀ κ', κ' ∈ KI → κ' ⊂ κ → κ' ∈ K) →
-  ([∗ set] κ' ∈ K, lft_inv_alive κ') -∗
-    ([∗ set] κ' ∈ KI, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ') ∗
-    (([∗ set] κ' ∈ KI, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ') -∗
-      ([∗ set] κ' ∈ K, lft_inv_alive κ')).
-Proof.
-  intros ?.
-  destruct (proj1 (subseteq_disjoint_union_L (filter (⊂ κ) KI) K)) as (K'&->&?).
-  { intros κ'. rewrite elem_of_filter. set_solver. }
-  rewrite big_sepS_union // big_sepS_filter. iIntros "[$ $]"; auto.
-Qed.
-
-Lemma ilft_create A I κ :
-  own_alft_auth A -∗ own_ilft_auth I -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
-      ==∗ ∃ A' I', ⌜is_Some (I' !! κ)⌝ ∗
-    own_alft_auth A' ∗ own_ilft_auth I' ∗ ▷ ([∗ set] κ ∈ dom _ I', lft_inv A' κ).
-Proof.
-  iIntros "HA HI Hinv".
-  destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
-  { iModIntro. iExists A, I. by iFrame. }
-  iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first done.
-  iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
-      (frac * dec_agree bor_state)))) as (γbor) "[Hbor Hbor']";
-    first by apply auth_valid_discrete_2.
-  iMod (own_alloc ((● ∅) :auth (gset_disj slice_name)))
-     as (γinh) "Hinh"; first by done.
-  set (γs := LftNames γbor γcnt γinh).
-  iMod (own_update with "HI") as "[HI Hγs]".
-  { apply auth_update_alloc,
-      (alloc_singleton_local_update _ κ (DecAgree γs)); last done.
-    by rewrite lookup_fmap HIκ. }
-  iDestruct "Hγs" as "#Hγs".
-  iAssert (own_cnt κ (● 0)) with "[Hcnt]" as "Hcnt".
-  { rewrite /own_cnt. iExists γs. by iFrame. }
-  iAssert (own_cnt κ (◯ 0)) with "[Hcnt']" as "Hcnt'".
-  { rewrite /own_cnt. iExists γs. by iFrame. }
-  iAssert (∀ b, lft_inh κ b True)%I with "[Hinh]" as "Hinh".
-  { iIntros (b). rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
-    iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iFrame. }
-  iAssert (lft_inv_dead κ ∧ lft_inv_alive κ)%I
-    with "[-HA HI Hinv]" as "Hdeadandalive".
-  { iSplit.
-    - rewrite /lft_inv_dead. iExists True%I. iFrame "Hcnt".
-      iSplitL "Hbor"; last by iApply "Hinh".
-      rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !to_gmap_empty.
-      iSplitL "Hbor". iExists γs. by iFrame. iApply box_alloc.
-    - rewrite lft_inv_alive_unfold. iExists True%I, True%I. iSplitL "Hbor".
-      { rewrite /lft_bor_alive. iExists ∅.
-        rewrite /to_borUR !fmap_empty big_sepM_empty.
-        iSplitR; [iApply box_alloc|]. iSplit=>//.
-        rewrite /own_bor. iExists γs. by iFrame. }
-      iSplitR "Hinh"; last by iApply "Hinh".
-      rewrite lft_vs_unfold. iExists 0. iFrame "Hcnt Hcnt'". auto. }
-  destruct (lft_alive_or_dead_in A κ) as [(Λ&?&HAΛ)|Haliveordead].
-  - iMod (own_update with "HA") as "[HA _]".
-    { apply auth_update_alloc,
-        (alloc_singleton_local_update _ Λ (Cinr ())); last done.
-      by rewrite lookup_fmap HAΛ. }
-    iModIntro. iExists (<[Λ:=false]>A), (<[κ:=γs]> I).
-    iSplit; first rewrite lookup_insert; eauto.
-    rewrite /own_ilft_auth /own_alft_auth /to_ilftUR /to_alftUR !fmap_insert.
-    iFrame "HA HI". rewrite dom_insert_L big_sepS_insert ?not_elem_of_dom //.
-    iSplitR "Hinv".
-    { rewrite /lft_inv. iNext. iRight. iSplit.
-      { by iDestruct "Hdeadandalive" as "[? _]". }
-      iPureIntro. exists Λ. rewrite lookup_insert; auto. }
-    iNext. iApply (@big_sepS_impl with "[$Hinv]").
-    rewrite /lft_inv. iIntros "!#"; iIntros (κ' ?%elem_of_dom)
-      "[[HA HA']|[HA HA']]"; iDestruct "HA'" as %HA.
-    + iLeft. iFrame "HA". iPureIntro. by apply lft_alive_in_insert.
-    + iRight. iFrame "HA". iPureIntro. by apply lft_dead_in_insert.
-  - iModIntro. iExists A, (<[κ:=γs]> I).
-    iSplit; first rewrite lookup_insert; eauto.
-    rewrite /own_ilft_auth /to_ilftUR fmap_insert. iFrame "HA HI".
-    rewrite dom_insert_L.
-    iApply @big_sepS_insert; first by apply not_elem_of_dom.
-    iFrame "Hinv". iNext. rewrite /lft_inv. destruct Haliveordead.
-    + iLeft. by iDestruct "Hdeadandalive" as "[_ $]".
-    + iRight. by iDestruct "Hdeadandalive" as "[$ _]".
-Qed.
-
-Lemma raw_bor_fake' E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ [†κ] ={E}=∗ raw_bor κ P.
-Proof.
-  iIntros (?) "#Hmgmt H†". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  iMod (ilft_create _ _ κ with "HA HI Hinv") as (A' I') "(Hκ & HA & HI & Hinv)".
-  iDestruct "Hκ" as %Hκ. rewrite /lft_dead. iDestruct "H†" as (Λ) "[% #H†]".
-  iDestruct (own_alft_auth_agree A' Λ false with "HA H†") as %EQAΛ.
-  iDestruct (@big_sepS_elem_of_acc with "Hinv")
-    as "[Hinv Hclose']"; first by apply elem_of_dom.
-  rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >%]|[Hinv >%]]".
-  { unfold lft_alive_in in *; naive_solver. }
-  rewrite /lft_inv_dead; iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
-  iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
-  iFrame. iApply "Hclose". iExists A', I'. iFrame. iNext. iApply "Hclose'".
-  rewrite /lft_inv /lft_inv_dead. iRight. iFrame. eauto.
-Qed.
-
-Lemma bor_fake E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
-Proof.
-  iIntros (?) "#Hmgmt H†". iMod (raw_bor_fake' with "Hmgmt H†"); first done.
-  iModIntro. unfold bor. iExists κ. iFrame. by rewrite -lft_incl_refl.
-Qed.
-
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
   let Iinv := (
     own_ilft_auth I ∗
@@ -146,7 +36,8 @@ Proof.
   iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first solve_ndisj.
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
-  iDestruct (lft_inv_alive_acc (dom _ I) _ κ with "Halive") as "[Halive Halive']".
+  iDestruct (big_sepS_filter_acc (⊂ κ) _ _ (dom _ I) with "Halive")
+    as "[Halive Halive']".
   { intros κ'. rewrite elem_of_dom. eauto. }
   iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
   { rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
@@ -242,7 +133,7 @@ Lemma lft_create E :
   ↑lftN ⊆ E →
   lft_ctx ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,⊤∖↑lftN}▷=∗ [†κ]).
 Proof.
-  iIntros (?) "#Hmgmt".
+  iIntros (?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   destruct (exist_fresh (dom (gset _) A)) as [Λ HΛ%not_elem_of_dom].
   iMod (own_update with "HA") as "[HA HΛ]".
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 28390da36d5397dfa9c4209ac1e2a4a9986e3b0e..b524fcae573a025f669f114101e06e3e86734cd3 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive accessors creation.
+From lrust.lifetime Require Export primitive accessors faking.
 From lrust.lifetime Require Export raw_reborrow.
 From iris.proofmode Require Import tactics.
 (* TODO: the name derived makes no sense: reborrow/bor_unnest, which is proven
diff --git a/theories/lifetime/faking.v b/theories/lifetime/faking.v
new file mode 100644
index 0000000000000000000000000000000000000000..59e53e3cb4cde7a7c12487bc0448ba263dec8c5e
--- /dev/null
+++ b/theories/lifetime/faking.v
@@ -0,0 +1,120 @@
+From lrust.lifetime Require Export primitive.
+From iris.algebra Require Import csum auth frac gmap dec_agree gset.
+From iris.base_logic Require Import big_op.
+From iris.base_logic.lib Require Import boxes.
+From iris.proofmode Require Import tactics.
+
+Section faking.
+Context `{invG Σ, lftG Σ}.
+Implicit Types κ : lft.
+
+Lemma ilft_create A I κ :
+  own_alft_auth A -∗ own_ilft_auth I -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
+      ==∗ ∃ A' I', ⌜is_Some (I' !! κ)⌝ ∗
+    own_alft_auth A' ∗ own_ilft_auth I' ∗ ▷ ([∗ set] κ ∈ dom _ I', lft_inv A' κ).
+Proof.
+  iIntros "HA HI Hinv".
+  destruct (decide (is_Some (I !! κ))) as [?|HIκ%eq_None_not_Some].
+  { iModIntro. iExists A, I. by iFrame. }
+  iMod (own_alloc (● 0 ⋅ ◯ 0)) as (γcnt) "[Hcnt Hcnt']"; first done.
+  iMod (own_alloc ((● ∅ ⋅ ◯ ∅) :auth (gmap slice_name
+      (frac * dec_agree bor_state)))) as (γbor) "[Hbor Hbor']";
+    first by apply auth_valid_discrete_2.
+  iMod (own_alloc ((● ∅) :auth (gset_disj slice_name)))
+     as (γinh) "Hinh"; first by done.
+  set (γs := LftNames γbor γcnt γinh).
+  iMod (own_update with "HI") as "[HI Hγs]".
+  { apply auth_update_alloc,
+      (alloc_singleton_local_update _ κ (DecAgree γs)); last done.
+    by rewrite lookup_fmap HIκ. }
+  iDestruct "Hγs" as "#Hγs".
+  iAssert (own_cnt κ (● 0)) with "[Hcnt]" as "Hcnt".
+  { rewrite /own_cnt. iExists γs. by iFrame. }
+  iAssert (own_cnt κ (◯ 0)) with "[Hcnt']" as "Hcnt'".
+  { rewrite /own_cnt. iExists γs. by iFrame. }
+  iAssert (∀ b, lft_inh κ b True)%I with "[Hinh]" as "Hinh".
+  { iIntros (b). rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
+    iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iFrame. }
+  iAssert (lft_inv_dead κ ∧ lft_inv_alive κ)%I
+    with "[-HA HI Hinv]" as "Hdeadandalive".
+  { iSplit.
+    - rewrite /lft_inv_dead. iExists True%I. iFrame "Hcnt".
+      iSplitL "Hbor"; last by iApply "Hinh".
+      rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !to_gmap_empty.
+      iSplitL "Hbor". iExists γs. by iFrame. iApply box_alloc.
+    - rewrite lft_inv_alive_unfold. iExists True%I, True%I. iSplitL "Hbor".
+      { rewrite /lft_bor_alive. iExists ∅.
+        rewrite /to_borUR !fmap_empty big_sepM_empty.
+        iSplitR; [iApply box_alloc|]. iSplit=>//.
+        rewrite /own_bor. iExists γs. by iFrame. }
+      iSplitR "Hinh"; last by iApply "Hinh".
+      rewrite lft_vs_unfold. iExists 0. iFrame "Hcnt Hcnt'". auto. }
+  destruct (lft_alive_or_dead_in A κ) as [(Λ&?&HAΛ)|Haliveordead].
+  - iMod (own_update with "HA") as "[HA _]".
+    { apply auth_update_alloc,
+        (alloc_singleton_local_update _ Λ (Cinr ())); last done.
+      by rewrite lookup_fmap HAΛ. }
+    iModIntro. iExists (<[Λ:=false]>A), (<[κ:=γs]> I).
+    iSplit; first rewrite lookup_insert; eauto.
+    rewrite /own_ilft_auth /own_alft_auth /to_ilftUR /to_alftUR !fmap_insert.
+    iFrame "HA HI". rewrite dom_insert_L big_sepS_insert ?not_elem_of_dom //.
+    iSplitR "Hinv".
+    { rewrite /lft_inv. iNext. iRight. iSplit.
+      { by iDestruct "Hdeadandalive" as "[? _]". }
+      iPureIntro. exists Λ. rewrite lookup_insert; auto. }
+    iNext. iApply (@big_sepS_impl with "[$Hinv]").
+    rewrite /lft_inv. iIntros "!#"; iIntros (κ' ?%elem_of_dom)
+      "[[HA HA']|[HA HA']]"; iDestruct "HA'" as %HA.
+    + iLeft. iFrame "HA". iPureIntro. by apply lft_alive_in_insert.
+    + iRight. iFrame "HA". iPureIntro. by apply lft_dead_in_insert.
+  - iModIntro. iExists A, (<[κ:=γs]> I).
+    iSplit; first rewrite lookup_insert; eauto.
+    rewrite /own_ilft_auth /to_ilftUR fmap_insert. iFrame "HA HI".
+    rewrite dom_insert_L.
+    iApply @big_sepS_insert; first by apply not_elem_of_dom.
+    iFrame "Hinv". iNext. rewrite /lft_inv. destruct Haliveordead.
+    + iLeft. by iDestruct "Hdeadandalive" as "[_ $]".
+    + iRight. by iDestruct "Hdeadandalive" as "[$ _]".
+Qed.
+
+Lemma raw_bor_fake E q κ P :
+  ↑borN ⊆ E →
+  ▷?q lft_bor_dead κ ={E}=∗ ▷?q lft_bor_dead κ ∗ raw_bor κ P.
+Proof.
+  iIntros (?). rewrite /lft_bor_dead. iDestruct 1 as (B Pinh) "[>HB● Hbox]".
+  iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & #Hslice & Hbox)".
+  iMod (own_bor_update with "HB●") as "[HB● H◯]".
+  { eapply auth_update_alloc,
+      (alloc_singleton_local_update _ _ (1%Qp, DecAgree Bor_in)); last done.
+    by do 2 eapply lookup_to_gmap_None. }
+  rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "Hâ—¯".
+  - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
+  - iExists γ. by iFrame.
+Qed.
+
+Lemma raw_bor_fake' E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ [†κ] ={E}=∗ raw_bor κ P.
+Proof.
+  iIntros (?) "#LFT H†". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
+  iMod (ilft_create _ _ κ with "HA HI Hinv") as (A' I') "(Hκ & HA & HI & Hinv)".
+  iDestruct "Hκ" as %Hκ. rewrite /lft_dead. iDestruct "H†" as (Λ) "[% #H†]".
+  iDestruct (own_alft_auth_agree A' Λ false with "HA H†") as %EQAΛ.
+  iDestruct (@big_sepS_elem_of_acc with "Hinv")
+    as "[Hinv Hclose']"; first by apply elem_of_dom.
+  rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >%]|[Hinv >%]]".
+  { unfold lft_alive_in in *; naive_solver. }
+  rewrite /lft_inv_dead; iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
+  iMod (raw_bor_fake _ true _ P with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
+  iFrame. iApply "Hclose". iExists A', I'. iFrame. iNext. iApply "Hclose'".
+  rewrite /lft_inv /lft_inv_dead. iRight. iFrame. eauto.
+Qed.
+
+Lemma bor_fake E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ [†κ] ={E}=∗ &{κ}P.
+Proof.
+  iIntros (?) "#LFT H†". iMod (raw_bor_fake' with "LFT H†"); first done.
+  iModIntro. unfold bor. iExists κ. iFrame. iApply lft_incl_refl.
+Qed.
+End faking.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 5514cece8082e673483474df0681e97a63fd45a7..0f2ab24052e00a46ca8b17252355609e389ee778 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -339,26 +339,11 @@ Proof.
   rewrite /idx_bor. iIntros "#Hκκ' [#? $]". by iApply (lft_incl_trans with "Hκκ'").
 Qed.
 
-Lemma raw_bor_fake E q κ P :
-  ↑borN ⊆ E →
-  ▷?q lft_bor_dead κ ={E}=∗ ▷?q lft_bor_dead κ ∗ raw_bor κ P.
-Proof.
-  iIntros (?). rewrite /lft_bor_dead. iDestruct 1 as (B Pinh) "[>HB● Hbox]".
-  iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & #Hslice & Hbox)".
-  iMod (own_bor_update with "HB●") as "[HB● H◯]".
-  { eapply auth_update_alloc,
-      (alloc_singleton_local_update _ _ (1%Qp, DecAgree Bor_in)); last done.
-    by do 2 eapply lookup_to_gmap_None. }
-  rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "Hâ—¯".
-  - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
-  - iExists γ. by iFrame.
-Qed.
-
 (* Inheritance *)
-Lemma lft_inh_acc E κ P Q :
+Lemma lft_inh_extend E κ P Q :
   ↑inhN ⊆ E →
   ▷ lft_inh κ false Q ={E}=∗ ▷ lft_inh κ false (P ∗ Q) ∗
-     (∀ I, own_ilft_auth I -∗ ⌜is_Some (I !! κ)⌝) ∧
+     (∀ I, own_ilft_auth I -∗ ⌜is_Some (I !! κ)⌝) ∗
      (∀ Q', ▷ lft_inh κ true Q' ={E}=∗ ∃ Q'',
             ▷ ▷ (Q' ≡ (P ∗ Q'')) ∗ ▷ P ∗ ▷ lft_inh κ true Q'').
 Proof.
@@ -371,8 +356,9 @@ Proof.
   iModIntro. iSplitL "Hbox HE".
   { iNext. rewrite /lft_inh. iExists ({[γE]} ∪ PE).
     rewrite to_gmap_union_singleton. iFrame. }
-  clear dependent PE. iSplit.
-  { iIntros (I) "HI". iApply (own_inh_auth with "HI HEâ—¯"). }
+  clear dependent PE. rewrite -(left_id_L ∅ op (◯ GSet {[γE]})).
+  iDestruct "HEâ—¯" as "[HEâ—¯' HEâ—¯]". iSplitL "HEâ—¯'".
+  { iIntros (I) "HI". iApply (own_inh_auth with "HI HEâ—¯'"). }
   iIntros (Q'). rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
   iDestruct (own_inh_valid_2 with "HE HEâ—¯")
     as %[Hle%gset_disj_included _]%auth_valid_discrete_2.
diff --git a/theories/lifetime/raw_reborrow.v b/theories/lifetime/raw_reborrow.v
index 95ea373a09ac547f94eb358a8540c399ca0ba6e3..32c27b7c8cc7234d84d72d0b0cb549a17f18fc77 100644
--- a/theories/lifetime/raw_reborrow.v
+++ b/theories/lifetime/raw_reborrow.v
@@ -1,4 +1,5 @@
-From lrust.lifetime Require Export primitive creation.
+From lrust.lifetime Require Export primitive.
+From lrust.lifetime Require Import faking.
 From iris.algebra Require Import csum auth frac gmap dec_agree gset.
 From iris.base_logic Require Import big_op.
 From iris.base_logic.lib Require Import boxes.
@@ -18,7 +19,7 @@ Lemma raw_bor_unnest E A I Pb Pi P κ i κ' :
   κ ⊂ κ' →
   lft_alive_in A κ' →
   Iinv -∗ idx_bor_own 1 (κ, i) -∗ slice borN i P -∗ ▷ lft_bor_alive κ' Pb -∗
-  ▷ lft_vs κ' (idx_bor_own 1 (κ, i) ∗ (*slice borN i P ∗*) Pb) Pi ={E}=∗ ∃ Pb',
+  ▷ lft_vs κ' (idx_bor_own 1 (κ, i) ∗ Pb) Pi ={E}=∗ ∃ Pb',
     Iinv ∗ raw_bor κ' P ∗ ▷ lft_bor_alive κ' Pb' ∗ ▷ lft_vs κ' Pb' Pi.
 Proof.
   iIntros (? Iinv Hκκ' Haliveκ') "(HI & Hκ) Hi #Hislice Hκalive' Hvs".
@@ -27,8 +28,7 @@ Proof.
   { 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 %?.
-  (* FIXME RJ: This is ugly. *)
-  assert (κ ⊆ κ'). { apply strict_spec_alt in Hκκ'. naive_solver. }
+  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;
@@ -107,7 +107,7 @@ Lemma raw_rebor E κ κ' P :
 Proof.
   rewrite /lft_ctx. iIntros (??) "#LFT Hκ".
   destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iFrame. iIntros "!> #Hκ†". iMod (raw_bor_fake' with "LFT Hκ†"); done. }
+  { 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)".
@@ -120,32 +120,30 @@ Proof.
     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. }
+    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]".
-  iMod (lft_inh_acc _ _ (idx_bor_own 1 (κ, i)) with "Hinh")
-    as "[Hinh Hinh_close]"; first solve_ndisj.
+  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]".
   { rewrite elem_of_difference elem_of_dom not_elem_of_singleton. done. }
-  iMod (raw_bor_unnest _ _ _ _ (idx_bor_own 1 (κ, i) ∗ Pi)%I with "[$HI $Hκ] Hi Hislice Hbor [Hvs]")
+  iMod (raw_bor_unnest _ _ _ _ (idx_bor_own 1 (κ, i) ∗ Pi)%I
+    with "[$HI $Hκ] Hi Hislice Hbor [Hvs]")
     as (Pb') "([HI Hκ] & $ & Halive & Hvs)"; [solve_ndisj|done|done|..].
   { iNext. by iApply lft_vs_frame. }
-  (* FIXME RJ: There should be sth. better than rewriting this. *)
-  rewrite {1}uPred.later_wand. iDestruct ("Hκclose" with "Hκ") as "Hinv".
+  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. }
-  iModIntro. iIntros "H†".
-  clear dependent A I Pb Pb' Pi.
+    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".
-  iAssert ⌜is_Some (I !! κ')⌝%I with "[#]" as %Hκ'.
-  { iDestruct "Hinh_close" as "[H _]". by iApply "H". }
-  iDestruct "Hinh_close" as "[_ Hinh_close]".
+  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 >%]]".
@@ -160,7 +158,6 @@ Proof.
       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 "∗#".
+    iModIntro. rewrite /raw_bor. iExists i. by iFrame.
 Qed.
-
 End rebor.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index f83e2b66dff821e87c89a9dbb1336e5e46e1df33..d2681f497e6c1dd8c07e669ebd393119233f7cca 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -3,8 +3,7 @@ From iris.base_logic Require Import big_op.
 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 reborrow borrow.
-
+From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 Import Types Perm.
 
 Section typing.