diff --git a/iris b/iris
index 42cf780adc3d61438701a106e50e07977c9b6abb..1bc26dc9822d6595df8d134fe365dd0356a4ac0b 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 42cf780adc3d61438701a106e50e07977c9b6abb
+Subproject commit 1bc26dc9822d6595df8d134fe365dd0356a4ac0b
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index af3550b31a09c89ddf19e8fe9f3f539bdec8a6fc..9289944881bb346bb25bc2d95f47e1123dff21db 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -69,10 +69,9 @@ Section definitions.
   Proof. apply _. Qed.
 End definitions.
 
-Typeclasses Opaque heap_ctx heap_mapsto heap_freeable.
+Typeclasses Opaque heap_ctx heap_mapsto heap_freeable heap_mapsto_vec.
 Instance: Params (@heap_mapsto) 4.
 Instance: Params (@heap_freeable) 5.
-Instance: Params (@heap_ctx) 2.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
@@ -128,7 +127,7 @@ Section heap.
   Proof. done. Qed.
 
   Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦∗{q} vl).
-  Proof. apply _. Qed.
+  Proof. rewrite /heap_mapsto_vec. apply _. Qed.
 
   Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
   Proof.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 2b327fe5e2e10700b7983ced6488ac73a85caf67..fb4d20e89692e4758c5581b997e1d180e304ea3e 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -14,7 +14,7 @@ Implicit Types Δ : envs (iResUR Σ).
 
 Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → 0 < n →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   (∀ l vl, n = length vl → ∃ Δ'',
     envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
       = Some Δ'' ∧
@@ -23,7 +23,7 @@ Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
 Proof.
   intros ???? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
   rewrite -always_and_sep_l. apply and_intro; first done.
-  rewrite into_later_env_sound; apply later_mono, forall_intro=> l;
+  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l;
   apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
   apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
   destruct (HΔ l vl) as (Δ''&?&HΔ'). done.
@@ -32,7 +32,7 @@ Qed.
 
 Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → n = length vl →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
   envs_delete i1 false Δ' = Δ'' →
   envs_lookup i2 Δ'' = Some (false, †l…n')%I →
@@ -44,13 +44,13 @@ Proof.
   intros ?? -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
   eapply wand_apply; first exact:wp_free. rewrite -!assoc -always_and_sep_l.
   apply and_intro; first done.
-  rewrite into_later_env_sound -!later_sep; apply later_mono.
+  rewrite into_laterN_env_sound -!later_sep; apply later_mono.
   do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True.
 Qed.
 
 Lemma tac_wp_read Δ Δ' E i l q v o Φ :
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
   (Δ' ⊢ |={E}=> Φ v) →
   Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
@@ -58,18 +58,18 @@ Proof.
   intros ??[->| ->]???.
   - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_na.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
+    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
       by apply later_mono, sep_mono_r, wand_mono.
   - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_sc.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
+    rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
       by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
 Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
   to_val e = Some v' →
   (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
-  IntoLaterEnvs Δ Δ' →
+  IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
   (Δ'' ⊢ |={E}=> Φ (LitV LitUnit)) →
@@ -78,14 +78,13 @@ Proof.
   intros ???[->| ->]????.
   - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_na.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
   - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_sc.
     rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
-    rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
+    rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
-
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
index 3c74848b7921d164cd994ccc18112a09ca7ad400..55c85215e5c75072dd15a3811d0ac813e9208b12 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/accessors.v
@@ -30,5 +30,4 @@ Lemma idx_bor_atomic_acc E q κ i P :
               ▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ idx_bor_own q i) ∨
               [†κ] ∗ (|={E∖↑lftN,E}=> idx_bor_own q i).
 Proof. Admitted.
-
 End accessors.
\ No newline at end of file
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index 239a0e222f8a0aa2d8148db7bbd977cec0bc8efb..e13617a05098e6f566fef1b9bdc032f28decc632 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -35,9 +35,9 @@ Proof.
           ?elem_of_dom // /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in.
   iDestruct "Hinv" as "[[[_ >%]|[Hinv >%]]Hclose']". naive_solver.
   iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
-  iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+  iMod (raw_bor_fake _ true with "Hdead") as (i) "[Hdead Hbor]"; first solve_ndisj.
   unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
-  iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame "∗%". eauto.
+  iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame. eauto.
 Qed.
 
 Lemma bor_create E κ P :
@@ -46,67 +46,77 @@ Lemma bor_create E κ P :
 Proof.
   iIntros (HE) "#Hmgmt HP". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
   iMod (ilft_create _ _ κ with "HI HA Hinv") as (A' I') "(Hκ & HI & HA & Hinv)".
-  iDestruct "Hκ" as %Hκ. rewrite big_sepS_later.
-  rewrite big_sepS_elem_of_acc
-          ?elem_of_dom // /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in.
-  iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]]Hclose']".
-  - rewrite lft_inv_alive_unfold /lft_bor_alive /lft_inh.
-    iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
-    iDestruct "Halive" as (B) "(HboxB & >HownB & HB)".
-    iDestruct "Hinh" as (PE) "[>HownE HboxE]".
-    iMod (box_insert_full with "HP HboxB") as (γB) "(HBlookup & HsliceB & HboxB)".
-      by solve_ndisj.
+  iDestruct "Hκ" as %Hκ. iDestruct (@big_sepS_later with "Hinv") as "Hinv".
+  iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose']".
+  { by apply elem_of_dom. }
+  rewrite {1}/lft_inv. iDestruct "Hinv" as "[[Hinv >%]|[Hinv >%]]".
+  - rewrite {1}lft_inv_alive_unfold;
+      iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
+    rewrite /lft_bor_alive; iDestruct "Halive" as (B) "(HboxB & >HownB & HB)".
+    rewrite /lft_inh; iDestruct "Hinh" as (PE) "[>HownE HboxE]".
+    iMod (slice_insert_full _ _ true with "HP HboxB")
+      as (γB) "(HBlookup & HsliceB & HboxB)"; first by solve_ndisj.
     rewrite lookup_fmap. iDestruct "HBlookup" as %HBlookup.
-    iMod (box_insert_empty _ P with "HboxE") as (γE) "(% & HsliceE & HboxE)".
+    iMod (slice_insert_empty _ _ true _ P with "HboxE")
+      as (γE) "(% & HsliceE & HboxE)".
     rewrite -(fmap_insert bor_filled _ _ Bor_in) -to_gmap_union_singleton.
     iMod (own_bor_update with "HownB") as "HownB".
-    { apply auth_update_alloc.
-      apply: (alloc_local_update _ _ γB (1%Qp, DecAgree Bor_in)); last done.
-      rewrite lookup_fmap. by destruct (B!!γB). }
+    { eapply auth_update_alloc,
+        (alloc_local_update _ _ γB (1%Qp, DecAgree Bor_in)); last done.
+      rewrite lookup_fmap. by destruct (B !! γB). }
     iMod (own_inh_update with "HownE") as "HownE".
     { by eapply auth_update_alloc, (gset_disj_alloc_empty_local_update _ {[γE]}),
-                disjoint_singleton_l, lookup_to_gmap_None. }
+        disjoint_singleton_l, lookup_to_gmap_None. }
     rewrite -fmap_insert own_bor_op own_inh_op insert_empty.
     iDestruct "HownB" as "[HB● HB◯]". iDestruct "HownE" as "[HE● HE◯]".
     iSpecialize ("Hclose'" with "[Hvs HboxE HboxB HB● HE● HB]").
-    { iNext. iLeft. iFrame "%". iExists _, (P ∗ Pi)%I.
+    { iNext. rewrite /lft_inv. iLeft. iFrame "%".
+      rewrite lft_inv_alive_unfold. iExists (P ∗ Pb)%I, (P ∗ Pi)%I.
       iSplitL "HboxB HB● HB"; last iSplitL "Hvs".
-      - iExists _. iFrame "HboxB HB●". rewrite big_sepM_insert /=.
-          by iFrame. by destruct (B !! γB).
+      - rewrite /lft_bor_alive.
+        iExists _. iFrame "HboxB HB●".
+        iApply @big_sepM_insert; first by destruct (B !! γB).
+        simpl. iFrame.
       - rewrite !lft_vs_unfold. iDestruct "Hvs" as (n) "[Hcnt Hvs]".
         iExists n. iFrame "Hcnt". iIntros (I'') "Hvsinv [$ HPb] H†".
         iApply ("Hvs" $! I'' with "Hvsinv HPb H†").
-      - iExists _. iFrame. }
+      - rewrite /lft_inh. iExists _. iFrame. }
     iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iExists _, _; iFrame|].
     iSplitL "HBâ—¯ HsliceB".
-    + unfold bor, raw_bor, idx_bor_own. iExists (κ, γB).
-      iSplitL "". by iApply lft_incl_refl. by iFrame.
-    + clear -HE. iIntros "!>H†".
+    + rewrite /bor /raw_bor /idx_bor_own. iExists (κ, γB); simpl.
+      iFrame. by iApply lft_incl_refl.
+    + clear -HE. iIntros "!> H†".
       iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
       iDestruct (own_inh_auth with "HI HE◯") as %Hκ.
-      rewrite big_sepS_elem_of_acc ?elem_of_dom //
-              /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in /lft_dead /lft_inh.
-      iDestruct "H†" as (Λ) "[% #H†]".
+      iDestruct (big_sepS_elem_of_acc _ _ κ with "Hinv") as "[Hinv Hclose']".
+      { by apply elem_of_dom. }
+      rewrite /lft_dead; iDestruct "H†" as (Λ) "[% #H†]".
       iDestruct (own_alft_auth_agree A Λ false with "HA H†") as %EQAΛ.
-      iDestruct "Hinv" as "[[[_ >%]|[Hinv >%]]Hclose']". naive_solver.
-      iDestruct "Hinv" as (Pinh) "(Hdead & >Hcnt & Hinh)".
-      iDestruct "Hinh" as (ESlices) "[>Hinh Hbox]".
+      rewrite {1}/lft_inv; iDestruct "Hinv" as "[[_ >%]|[Hinv >%]]".
+      { unfold lft_alive_in in *. naive_solver. }
+      rewrite /lft_inv_dead; iDestruct "Hinv" as (Pinh) "(Hdead & >Hcnt & Hinh)".
+      rewrite /lft_inh; iDestruct "Hinh" as (ESlices) "[>Hinh Hbox]".
       iDestruct (own_inh_valid_2 with "Hinh HEâ—¯")
         as %[Hle%gset_disj_included _]%auth_valid_discrete_2.
       rewrite <-elem_of_subseteq_singleton in Hle.
       iMod (own_inh_update with "[HE◯ Hinh]") as "HE●"; [|iApply own_inh_op; by iFrame|].
       { apply auth_update_dealloc, gset_disj_dealloc_local_update. }
-      iMod (box_delete_full with "HsliceE Hbox") as (Pinh') "($ & _ & Hbox)".
-        solve_ndisj. by rewrite lookup_to_gmap_Some.
-      iApply "Hclose". iExists _, _. iFrame. iNext. iApply "Hclose'". iRight. iFrame "%".
-      iExists _. iFrame. iExists _. iFrame.
+      iMod (slice_delete_full _ _ true with "HsliceE Hbox")
+        as (Pinh') "($ & _ & Hbox)"; first by solve_ndisj.
+      { by rewrite lookup_to_gmap_Some. }
+      iApply "Hclose". iExists A, I. iFrame. iNext. iApply "Hclose'".
+      rewrite /lft_inv. iRight. iFrame "%".
+      rewrite /lft_inv_dead. iExists Pinh'. iFrame.
+      rewrite /lft_inh. iExists _. iFrame.
       rewrite {1}(union_difference_L {[γE]} ESlices); last set_solver.
-      rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None. set_solver.
+      rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None.
+      set_solver +Hle.
   - iFrame "HP". iApply fupd_frame_r. iSplitR ""; last by auto.
-    iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)" .
-    iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+    rewrite /lft_inv_dead. iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)" .
+    iMod (raw_bor_fake _ true with "Hdead") as (i) "[Hdead Hbor]"; first solve_ndisj.
     unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
-    iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame "∗%". eauto.
+    iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iNext.
+    rewrite /lft_inv. iRight. rewrite /lft_inv_dead. iFrame. eauto.
 Qed.
 
 Lemma bor_sep E κ P Q :
@@ -125,8 +135,9 @@ Proof.
     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 (box_split with "Hslice Hbox") as (γ1 γ2) "(% & % & % & Hs1 & Hs2 & Hbox)".
-      solve_ndisj. by rewrite lookup_fmap EQB.
+    iMod (slice_split _ _ true with "Hslice Hbox")
+      as (γ1 γ2) "(% & % & % & Hs1 & Hs2 & Hbox)"; first solve_ndisj.
+    { by rewrite lookup_fmap EQB. }
     iCombine "Hown" "Hbor" as "Hbor". rewrite -own_bor_op.
     iMod (own_bor_update with "Hbor") as "Hbor".
     { etrans; last etrans.
@@ -153,8 +164,8 @@ Proof.
     + 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 with "Hdead") as (i1) "[Hdead Hbor1]". solve_ndisj.
-    iMod (raw_bor_fake with "Hdead") as (i2) "[Hdead Hbor2]". solve_ndisj.
+    iMod (raw_bor_fake _ true with "Hdead") as (i1) "[Hdead Hbor1]"; first solve_ndisj.
+    iMod (raw_bor_fake _ true with "Hdead") as (i2) "[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. }
@@ -190,8 +201,11 @@ Proof.
       iDestruct (own_bor_valid_2 with "Hbor1 Hbor2") as %Hj1j2%auth_valid_discrete.
       exfalso. revert Hj1j2. rewrite /= op_singleton singleton_valid.
       compute. tauto. }
-    iMod (box_combine with "Hslice1 Hslice2 Hbox") as (γ) "(% & Hslice & Hbox)".
-      solve_ndisj. done. by rewrite lookup_fmap EQB1. by rewrite lookup_fmap EQB2.
+    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.
@@ -215,11 +229,10 @@ Proof.
       rewrite lookup_delete_ne //.
     + rewrite -fmap_None -lookup_fmap !fmap_delete //.
   - iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)".
-    iMod (raw_bor_fake with "Hdead") as (i) "[Hdead Hbor]". solve_ndisj.
+    iMod (raw_bor_fake _ true with "Hdead") as (i) "[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
+End borrow.
diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index 0b9e20bff843a7af269bebc58cff24fecc067b78..9dd4c7becc3e12c583f2b97f90fb9254270eb423 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -15,7 +15,7 @@ Lemma lft_inh_kill E κ Q :
 Proof.
   rewrite /lft_inh. iIntros (?) "[Hinh HQ]".
   iDestruct "Hinh" as (E') "[Hinh Hbox]".
-  iMod (box_fill_all with "Hbox HQ") as "?"=>//.
+  iMod (box_fill with "Hbox HQ") as "?"=>//.
   rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
 Qed.
 
@@ -124,7 +124,7 @@ Proof.
     rewrite /lft_inv_dead; iDestruct "Hdead" as (R) "(_ & Hcnt' & _)".
     iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
       as %[?%nat_included _]%auth_valid_discrete_2; omega. }
-  iMod (box_empty_all with "Hbox") as "[HP Hbox]"=>//; first solve_ndisj.
+  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']".
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 263a0af2d56d69a4f14e71e580b22201d4d61221..acbe01970072d88b18deebfa5614def5cced0ac1 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -12,7 +12,7 @@ Lemma bor_acc E q κ P :
 Proof.
   iIntros (?) "#LFT HP Htok".
   iMod (bor_acc_strong with "LFT HP Htok") as "[HP Hclose]"; first done.
-  iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP}!>_$".
+  iIntros "!> {$HP} HP". iApply "Hclose". by iIntros "{$HP} !> _ $".
 Qed.
 
 Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
@@ -40,7 +40,7 @@ Lemma bor_persistent P `{!PersistentP P} E κ q :
 Proof.
   iIntros (?) "#LFT Hb Htok".
   iMod (bor_acc with "LFT Hb Htok") as "[#HP Hob]"; first done.
-  by iMod ("Hob" with "HP") as "[_$]".
+  by iMod ("Hob" with "HP") as "[_ $]".
 Qed.
 
 Lemma lft_incl_acc E κ κ' q :
@@ -65,5 +65,4 @@ Proof.
   - iIntros (q) "?". iExists 1%Qp. iSplitR. by iApply lft_tok_static. auto.
   - iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
 Qed.
-
 End derived.
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index 91b9e902ab39a94ab521bcc6dda6826491b14167..310dd12bd291fe2112d9ceac8077d243c66819cf 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -8,48 +8,51 @@ Section rebor.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-Lemma raw_bor_fake E κ P :
+Lemma raw_bor_fake E q κ P :
   ↑borN ⊆ E →
-  ▷ lft_bor_dead κ ={E}=∗ ∃ i, ▷ lft_bor_dead κ ∗ raw_bor (κ, i) P.
+  ▷?q lft_bor_dead κ ={E}=∗ ∃ i, ▷?q lft_bor_dead κ ∗ raw_bor (κ, i) P.
 Proof.
   iIntros (?) "Hdead". rewrite /lft_bor_dead.
   iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
-  iMod (box_insert_empty _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
+  iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
   iMod (own_bor_update with "Hown") as "Hown".
-  { apply auth_update_alloc.
-    apply: (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
-    do 2 eapply lookup_to_gmap_None. by eauto. }
-  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own. iExists _.
-  iDestruct "Hown" as "[H● H◯]". iSplitL "H● Hbox"; last by eauto.
-  iExists _, _. rewrite -!to_gmap_union_singleton. by iFrame.
+  { eapply auth_update_alloc,
+      (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
+    by do 2 eapply lookup_to_gmap_None. }
+  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own /=. iExists γ.
+  iDestruct "Hown" as "[H● $]". iFrame "Hslice". iModIntro. iNext.
+  iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
 Qed.
 
 Lemma raw_bor_unnest A I Pb Pi P κ κ' i :
   let Iinv := (
     own_ilft_auth I ∗
-    ▷ ([∗ set] κ ∈ dom _ I ∖ {[ κ' ]}, lft_inv A κ))%I in
+    ▷ [∗ set] κ ∈ dom _ I ∖ {[κ']}, lft_inv A κ)%I in
   κ ⊆ κ' →
   lft_alive_in A κ' →
   Iinv -∗ raw_bor (κ,i) P -∗ ▷ lft_bor_alive κ' Pb -∗
   ▷ lft_vs κ' (Pb ∗ raw_bor (κ,i) P) Pi ={↑borN}=∗ ∃ Pb' j,
     Iinv ∗ raw_bor (κ',j) P ∗ ▷ lft_bor_alive κ' Pb' ∗ ▷ lft_vs κ' Pb' Pi.
 Proof.
-  iIntros (Iinv Hκκ' Haliveκ') "(HI & HA) Hraw Hκalive' Hvs".
+  iIntros (Iinv Hκκ' Haliveκ') "(HI● & HI) Hraw Hκalive' Hvs".
   destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iModIntro. iExists Pb, i. rewrite /Iinv. iFrame "HI HA Hκalive' Hraw".
+  { iModIntro. iExists Pb, i. rewrite /Iinv. iFrame "HI● HI Hκalive' Hraw".
     iNext. rewrite !lft_vs_unfold. iDestruct "Hvs" as (n) "[Hn Hvs]".
     iExists n. iFrame "Hn". clear Iinv I.
-    iIntros (I) "Hinv HPb Hdead". admit. }
+    iIntros (I). rewrite lft_vs_inv_unfold. iIntros "(Hdead & $ & HI) HPb Hκ†".
+    iMod (raw_bor_fake _ false _ P with "Hdead") as (i') "?"; first solve_ndisj.
+    (* We get the existential too late *)
+    admit. }
   assert (κ ⊂ κ') by (by apply strict_spec_alt).
   rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hcnt Hvs]".
   iMod (own_cnt_update with "Hcnt") as "Hcnt".
   { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
   rewrite own_cnt_op; iDestruct "Hcnt" as "[Hcnt Hcnt1]".
   rewrite {1}/raw_bor /idx_bor_own /=. iDestruct "Hraw" as "[Hbor #Hislice]".
-  iDestruct (own_bor_auth with "HI Hbor") as %?.
+  iDestruct (own_bor_auth with "HI● Hbor") as %?.
   rewrite big_sepS_later.
-  iDestruct (big_sepS_elem_of_acc _ (dom (gset lft) I ∖ _) κ
-    with "HA") as "[HAκ HA]".
+  iDestruct (big_sepS_elem_of_acc _ (dom (gset lft) I ∖ _) κ with "HI")
+    as "[HAκ HI]".
   { by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
   iDestruct (lft_inv_alive_in with "HAκ") as "Hκalive";
     first by eauto using lft_alive_in_subseteq.
@@ -58,14 +61,14 @@ Proof.
   rewrite {2}/lft_bor_alive; iDestruct "Hbor'" as (B) "(Hbox & >HκB & HB)".
   iDestruct (own_bor_valid_2 with "HκB Hbor")
     as %[HB%to_borUR_included _]%auth_valid_discrete_2.
-  iMod (box_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
+  iMod (slice_empty _ _ true with "Hislice Hbox") as "[HP Hbox]"; first done.
   { by rewrite lookup_fmap HB. }
   iMod (own_bor_update_2 with "HκB Hbor") as "HFOO".
   { eapply auth_update, singleton_local_update,
      (exclusive_local_update _ (1%Qp, DecAgree (Bor_rebor κ'))); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   rewrite own_bor_op. iDestruct "HFOO" as "[HκB Hrebor]".
-  iSpecialize ("HA" with "[Hcnt1 HB Hvs' Hinh' Hbox HκB]").
+  iSpecialize ("HI" with "[Hcnt1 HB Hvs' Hinh' Hbox HκB]").
   { iNext. rewrite /lft_inv. iLeft.
     iSplit; last by eauto using lft_alive_in_subseteq.
     rewrite lft_inv_alive_unfold. iExists Pb', Pi'. iFrame "Hvs' Hinh'".
@@ -77,14 +80,15 @@ Proof.
     iFrame; simpl; auto. }
   clear B HB Pb' Pi'.
   rewrite {1}/lft_bor_alive. iDestruct "Hκalive'" as (B) "(Hbox & >Hbor & HB)".
-  iMod (box_insert_full with "HP Hbox") as (j) "(HBj & #Hjslice & Hbox)"; first done.
+  iMod (slice_insert_full _ _ true with "HP Hbox")
+    as (j) "(HBj & #Hjslice & Hbox)"; first done.
   iDestruct "HBj" as %HBj. move: HBj; rewrite lookup_fmap fmap_None=> HBj.
   iMod (own_bor_update with "Hbor") as "HFOO".
   { apply auth_update_alloc,
      (alloc_singleton_local_update _ j (1%Qp, DecAgree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HBj. }
   rewrite own_bor_op. iDestruct "HFOO" as "[HκB Hj]".
-  iModIntro. iExists (P ∗ Pb)%I, j. rewrite /Iinv. iFrame "HI HA".
+  iModIntro. iExists (P ∗ Pb)%I, j. rewrite /Iinv. iFrame "HI● HI".
   iSplitL "Hj".
   { rewrite /raw_bor /idx_bor_own. by iFrame. }
   iSplitL "HB HκB Hbox".
@@ -107,10 +111,8 @@ Proof.
      (exclusive_local_update _ (1%Qp, DecAgree Bor_in)); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   rewrite own_bor_op. iDestruct "HFOO" as "[Hbor Hrebor]".
-  iMod (box_fill with "Hislice HP [Hbox]") as "Hbox". 3: by iNext. solve_ndisj.
-  by rewrite lookup_fmap HB.
-iAssert (box borN (<[i:=true]> (bor_filled <$> B')) Pb') with "[Hbox]" as "Hbox".
-admit.
+  iMod (slice_fill _ _ false with "Hislice HP Hbox") as "Hbox"; first by solve_ndisj.
+  { by rewrite lookup_fmap HB. }
   iDestruct (@big_sepM_delete with "HB") as "[Hκ HB]"; first done.
   rewrite /=; iDestruct "Hκ" as "[% Hcnt]".
   iMod ("Hvs" $! I with "[Hdead HI Hκs Hbox Hvs' Hinh Hbor HB]
@@ -122,12 +124,10 @@ admit.
     iExists (<[i:=Bor_in]>B'). rewrite /to_borUR !fmap_insert. iFrame.
     rewrite -insert_delete big_sepM_insert ?lookup_delete //=. by iFrame. }
   { rewrite /raw_bor /idx_bor_own /=. iFrame; auto. }
-    iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus.
-(* auth_frag_op. *)
-
+  iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
+  by iFrame.
 Admitted.
 
-
 Lemma raw_rebor E κ κ' i P :
   ↑lftN ⊆ E → κ ⊆ κ' →
   lft_ctx -∗ raw_bor (κ, i) P ={E}=∗
@@ -155,5 +155,4 @@ Lemma bor_unnest E κ κ' P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
 Proof. Admitted.
-
 End rebor.