diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
index cae3177ef072fd0b82a1c02e7825ed38c8480871..db2fa8ecbac8871ab443618187e566d00daf1598 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/accessors.v
@@ -169,7 +169,7 @@ Lemma bor_acc_strong E q κ P :
     ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
 Proof.
   unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
-  iDestruct "Hbor" as (i) "(#Hle & Hbor & #Hs)".
+  iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)".
   iMod (lft_incl_acc with "Hle Htok") as (q') "[Htok Hclose]". solve_ndisj.
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
   iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
@@ -177,12 +177,12 @@ Proof.
           /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in lft_inv_alive_unfold.
   iDestruct "Hinv" as "[[[Hinv >%]|[Hinv >%]] Hclose'']".
   - iDestruct "Hinv" as (Pb Pi) "(Halive & Hvs & Hinh)".
-    iMod (bor_open_internal with "Hs Halive Hbor Htok") as "(Halive & Hbor & $)".
+    iMod (bor_open_internal _ _ (κ'', s'') with "Hs Halive Hbor Htok") as "(Halive & Hbor & $)".
       solve_ndisj.
     iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
     { iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
       iLeft. iFrame "%". iExists _, _. iFrame. }
-    iExists (i.1). iFrame "#". iIntros "!>*HQ HvsQ". clear -HE.
+    iExists κ''. iFrame "#". iIntros "!>*HQ HvsQ". clear -HE.
     iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
     iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
     rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -214,8 +214,8 @@ Proof.
       iMod ("Hclose'" with "[-Hbor Htok Hclose]") as "_".
       { iExists _, _. iFrame. rewrite big_sepS_later /lft_bor_alive. iApply "Hclose''".
         iLeft. iFrame "%". iExists _, _. iFrame. }
-      iMod ("Hclose" with "Htok") as "$". iExists (i.1, j). iFrame "∗#".
-      iApply lft_incl_refl.
+      iMod ("Hclose" with "Htok") as "$". iExists κ''. iModIntro.
+      iSplit; first by iApply lft_incl_refl. iExists j. iFrame "∗#".
     + iDestruct "Hinv" as (?) "[Hinv _]". iDestruct "Hinv" as (B ?) "[>Hinv _]".
       iDestruct (own_bor_valid_2 with "Hinv Hbor")
         as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
@@ -232,8 +232,8 @@ Lemma bor_acc_atomic_strong E κ P :
       ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
     [†κ] ∗ |={E∖↑lftN,E}=> True.
 Proof.
-  unfold bor, raw_bor. iIntros (HE) "#LFT Hbor".
-  iDestruct "Hbor" as (i) "(#Hle & Hbor & #Hs)".
+  iIntros (HE) "#LFT Hbor". rewrite bor_unfold_idx /idx_bor /bor /raw_bor.
+  iDestruct "Hbor" as (i) "((#Hle & #Hs) & Hbor)".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
   iDestruct (own_bor_auth with "HI [Hbor]") as %Hκ'. by unfold idx_bor_own.
   rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -251,18 +251,20 @@ Proof.
     iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs HvsQ") as "Hvs".
     iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
       solve_ndisj.
-    iExists (i.1, j). iFrame "∗#".
     iMod (own_bor_update_2 with "Hown Hbor") as "Hown".
     { apply auth_update. etrans.
       - apply delete_singleton_local_update, _.
       - apply (alloc_singleton_local_update _ j (1%Qp, DecAgree (Bor_in))); last done.
         rewrite -fmap_delete lookup_fmap fmap_None
                 -fmap_None -lookup_fmap fmap_delete //. }
-    rewrite own_bor_op -lft_incl_refl. iDestruct "Hown" as "[Hown $]".
-    iApply "Hclose'". iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
-    iLeft. iFrame "%". iExists _, _. iFrame.
+    rewrite own_bor_op. iDestruct "Hown" as "[H● H◯]".
+    iMod ("Hclose'" with "[- Hâ—¯]"); last first.
+    { iModIntro. iExists (i.1). iSplit; first by iApply lft_incl_refl.
+      iExists j. iFrame. done. }
+    iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
+    iLeft. iFrame "%". iExists _, _. iFrame. iNext.
     rewrite -!fmap_delete -fmap_insert -(fmap_insert _ _ _ Bor_in).
-    iExists _. iFrame "Hbox Hown".
+    iExists _. iFrame "Hbox H●".
     rewrite big_sepM_insert. by rewrite big_sepM_delete.
       by rewrite -fmap_None -lookup_fmap fmap_delete.
   - iRight. iMod (create_dead with "HA") as "[HA #H†]". done.
diff --git a/theories/lifetime/borrow.v b/theories/lifetime/borrow.v
index 5a97f4f7cd5a0f3f16c118c8250278e42e6718e5..c4e5f040eb40bf8da48a19b218d4feee5cbc2240 100644
--- a/theories/lifetime/borrow.v
+++ b/theories/lifetime/borrow.v
@@ -10,8 +10,11 @@ Implicit Types κ : lft.
 
 Lemma bor_unfold_idx κ P : &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
 Proof.
-  rewrite /bor /raw_bor /idx_bor /bor_idx. f_equiv. intros [??].
-  rewrite -assoc. f_equiv. by rewrite comm.
+  rewrite /bor /raw_bor /idx_bor /bor_idx. iProof; iSplit.
+  - iIntros "H". iDestruct "H" as (κ') "[? Hraw]". iDestruct "Hraw" as (s) "[??]".
+    iExists (κ', s). by iFrame.
+  - iIntros "H". iDestruct "H" as ([κ' s]) "[[??]?]". iExists κ'. iFrame.
+    iExists s. by iFrame.
 Qed.
 
 Lemma bor_shorten κ κ' P: κ ⊑ κ' -∗ &{κ'}P -∗ &{κ}P.
@@ -35,8 +38,8 @@ 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 _ true with "Hdead") as (i) "[Hdead Hbor]"; first solve_ndisj.
-  unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
+  iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
+  unfold bor. iExists κ. iFrame. rewrite -lft_incl_refl -big_sepS_later.
   iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iRight. iFrame. eauto.
 Qed.
 
@@ -83,8 +86,8 @@ Proof.
       - rewrite /lft_inh. iExists _. iFrame. }
     iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iExists _, _; iFrame|].
     iSplitL "HBâ—¯ HsliceB".
-    + rewrite /bor /raw_bor /idx_bor_own. iExists (κ, γB); simpl.
-      iFrame. by iApply lft_incl_refl.
+    + rewrite /bor /raw_bor /idx_bor_own. iExists κ; simpl.
+      iModIntro. iSplit; first by iApply lft_incl_refl. iExists γB. by iFrame.
     + clear -HE. iIntros "!> H†".
       iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
       iDestruct (own_inh_auth with "HI HE◯") as %Hκ.
@@ -113,8 +116,8 @@ Proof.
       set_solver+.
   - iFrame "HP". iApply fupd_frame_r. iSplitR ""; last by auto.
     rewrite /lft_inv_dead. iDestruct "Hinv" as (Pinh) "(Hdead & Hcnt & Hinh)" .
-    iMod (raw_bor_fake _ true with "Hdead") as (i) "[Hdead Hbor]"; first solve_ndisj.
-    unfold bor. iExists (κ, i). iFrame. rewrite -lft_incl_refl -big_sepS_later.
+    iMod (raw_bor_fake _ true with "Hdead") as "[Hdead Hbor]"; first solve_ndisj.
+    unfold bor. iExists κ. iFrame. rewrite -lft_incl_refl -big_sepS_later.
     iApply "Hclose". iExists _, _. iFrame. iApply "Hclose'". iNext.
     rewrite /lft_inv. iRight. rewrite /lft_inv_dead. iFrame. eauto.
 Qed.
@@ -125,7 +128,7 @@ Lemma bor_sep 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 ([κ' s]) "[#Hκκ' [Hbor Hslice]]".
+  iDestruct "HP" as (κ') "[#Hκκ' Htmp]". iDestruct "Htmp" as (s) "[Hbor Hslice]".
   iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
   rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
           /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in. simpl.
@@ -152,9 +155,9 @@ Proof.
                 -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 (κ', γ1). iFrame "∗#". }
+    { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ1. iFrame. }
     iAssert (&{κ}Q)%I with "[H◯2 Hs2]" as "$".
-    { rewrite /bor /raw_bor /idx_bor_own. iExists (κ', γ2). iFrame "∗#". }
+    { rewrite /bor /raw_bor /idx_bor_own. iExists κ'. iFrame "#". iExists γ2. iFrame. }
     iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
     iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
     rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
@@ -163,12 +166,12 @@ 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 _ 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 (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.
+    unfold bor. iSplitL "Hbor1"; iExists _; eauto.
 Qed.
 
 Lemma bor_combine E κ P Q :
@@ -176,14 +179,13 @@ Lemma bor_combine E κ P Q :
   lft_ctx -∗ &{κ} P -∗ &{κ} Q ={E}=∗ &{κ} (P ∗ Q).
 Proof.
   iIntros (?) "#Hmgmt HP HQ". rewrite {1 2}/bor.
-  iDestruct "HP" as ([κ1 i1]) "[#Hκ1 Hbor1]".
-  iDestruct "HQ" as ([κ2 i2]) "[#Hκ2 Hbor2]".
-  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor1") as (j1) "[Hbor1 _]".
+  iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
+  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor1") as "[Hbor1 _]".
     done. by apply gmultiset_union_subseteq_l.
-  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor2") as (j2) "[Hbor2 _]".
+  iMod (raw_rebor _ _ (κ1 ∪ κ2) with "Hmgmt Hbor2") as "[Hbor2 _]".
     done. by apply gmultiset_union_subseteq_r.
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
-  iDestruct "Hbor1" as "[Hbor1 Hslice1]". iDestruct "Hbor2" as "[Hbor2 Hslice2]".
+  iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
   iDestruct (own_bor_auth with "HI Hbor1") as %Hκ'.
   rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
           /lfts_inv /lft_inv /lft_inv_dead /lft_alive_in. simpl.
@@ -217,8 +219,9 @@ Proof.
                 -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, γ). iFrame.
-      iApply (lft_incl_glb with "Hκ1 Hκ2"). }
+    { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2). 
+      iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
+      iExists γ. iFrame. } 
     iApply "Hclose". iExists A, I. iFrame. rewrite big_sepS_later.
     iApply "Hclose'". iLeft. iFrame "%". iExists Pb, Pi. iFrame. iExists _.
     rewrite /to_borUR -!fmap_delete -!fmap_insert. iFrame "Hbox H●".
@@ -228,10 +231,10 @@ Proof.
       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 (i) "[Hdead Hbor]"; first solve_ndisj.
+    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").
+    unfold bor. iExists _. iFrame. iApply (lft_incl_glb with "Hκ1 Hκ2").
 Qed.
 End borrow.
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index 8441937fb2892c5c56c9d281cf57bc453efb3b12..995a2fb3d3f0439feb92902d31792376b2eaf8d6 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -174,10 +174,10 @@ Section defs.
     own_bor (i.1) (â—¯ {[ i.2 := (q,DecAgree Bor_in) ]}).
   Definition idx_bor (κ : lft) (i : bor_idx) (P : iProp Σ) : iProp Σ :=
     (lft_incl κ (i.1) ∗ slice borN (i.2) P)%I.
-  Definition raw_bor (i : bor_idx) (P : iProp Σ) : iProp Σ :=
-    (idx_bor_own 1 i ∗ slice borN (i.2) P)%I.
+  Definition raw_bor (κ : lft) (P : iProp Σ) : iProp Σ :=
+    (∃ s : slice_name, idx_bor_own 1 (κ, s) ∗ slice borN s P)%I.
   Definition bor (κ : lft) (P : iProp Σ) : iProp Σ :=
-    (∃ i, lft_incl κ (i.1) ∗ raw_bor i P)%I.
+    (∃ κ', lft_incl κ κ' ∗ raw_bor κ' P)%I.
 End defs.
 
 Instance: Params (@lft_bor_alive) 4.
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
index 310dd12bd291fe2112d9ceac8077d243c66819cf..bba7edeeb34ad2a867db6b5913015c6c76ad7dc6 100644
--- a/theories/lifetime/rebor.v
+++ b/theories/lifetime/rebor.v
@@ -10,45 +10,47 @@ Implicit Types κ : lft.
 
 Lemma raw_bor_fake E q κ P :
   ↑borN ⊆ E →
-  ▷?q lft_bor_dead κ ={E}=∗ ∃ i, ▷?q lft_bor_dead κ ∗ raw_bor (κ, i) P.
+  ▷?q lft_bor_dead κ ={E}=∗ ▷?q lft_bor_dead κ ∗ raw_bor κ P.
 Proof.
   iIntros (?) "Hdead". rewrite /lft_bor_dead.
   iDestruct "Hdead" as (B Pinh) "[>Hown Hbox]".
-  iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & Hslice & Hbox)".
+  iMod (slice_insert_empty _ _ _ _ P with "Hbox") as (γ) "(% & #Hslice & Hbox)".
   iMod (own_bor_update with "Hown") as "Hown".
   { eapply auth_update_alloc,
       (alloc_local_update _ _ _ (1%Qp, DecAgree Bor_in)); last done.
     by do 2 eapply lookup_to_gmap_None. }
-  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own /=. iExists γ.
-  iDestruct "Hown" as "[H● $]". iFrame "Hslice". iModIntro. iNext.
-  iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
+  rewrite own_bor_op insert_empty /bor /raw_bor /idx_bor_own /=. 
+  iModIntro. iDestruct "Hown" as "[H● H◯]". iSplitR "H◯".
+  - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
+  - iExists γ. by iFrame.
 Qed.
 
-Lemma raw_bor_unnest A I Pb Pi P κ κ' i :
+Lemma raw_bor_unnest A I Pb Pi P κ κ' :
   let Iinv := (
     own_ilft_auth I ∗
     ▷ [∗ set] κ ∈ dom _ I ∖ {[κ']}, lft_inv A κ)%I in
   κ ⊆ κ' →
   lft_alive_in A κ' →
-  Iinv -∗ raw_bor (κ,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.
+  Iinv -∗ raw_bor κ P -∗ ▷ lft_bor_alive κ' Pb -∗
+  ▷ lft_vs κ' (Pb ∗ raw_bor κ P) Pi ={↑borN}=∗ ∃ Pb',
+    Iinv ∗ raw_bor κ' P ∗ ▷ lft_bor_alive κ' Pb' ∗ ▷ lft_vs κ' Pb' Pi.
 Proof.
   iIntros (Iinv Hκκ' Haliveκ') "(HI● & HI) Hraw Hκalive' Hvs".
   destruct (decide (κ = κ')) as [<-|Hκneq].
-  { iModIntro. iExists Pb, i. rewrite /Iinv. iFrame "HI● HI Hκalive' Hraw".
+  { iModIntro. iExists Pb. rewrite /Iinv. iFrame "HI● HI Hκalive' Hraw".
     iNext. rewrite !lft_vs_unfold. iDestruct "Hvs" as (n) "[Hn Hvs]".
     iExists n. iFrame "Hn". clear Iinv I.
-    iIntros (I). rewrite 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. }
+    iIntros (I). rewrite {1}lft_vs_inv_unfold. iIntros "(Hdead & HI & Hκs) HPb #Hκ†".
+    iMod (raw_bor_fake _ false _ P with "Hdead") as "[Hdead Hraw]"; first solve_ndisj.
+    iApply ("Hvs" $! I with "[Hdead HI Hκs] [HPb Hraw] Hκ†").
+    - rewrite lft_vs_inv_unfold. by iFrame.
+    - iNext. by iFrame. }
   assert (κ ⊂ κ') by (by apply strict_spec_alt).
   rewrite lft_vs_unfold. iDestruct "Hvs" as (n) "[>Hcnt Hvs]".
   iMod (own_cnt_update with "Hcnt") as "Hcnt".
   { apply auth_update_alloc, (nat_local_update _ 0 (S n) 1); omega. }
   rewrite own_cnt_op; iDestruct "Hcnt" as "[Hcnt Hcnt1]".
-  rewrite {1}/raw_bor /idx_bor_own /=. iDestruct "Hraw" as "[Hbor #Hislice]".
+  rewrite {1}/raw_bor /idx_bor_own /=. iDestruct "Hraw" as (i) "[Hbor #Hislice]".
   iDestruct (own_bor_auth with "HI● Hbor") as %?.
   rewrite big_sepS_later.
   iDestruct (big_sepS_elem_of_acc _ (dom (gset lft) I ∖ _) κ with "HI")
@@ -88,9 +90,9 @@ Proof.
      (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● HI".
+  iModIntro. iExists (P ∗ Pb)%I. rewrite /Iinv. iFrame "HI● HI".
   iSplitL "Hj".
-  { rewrite /raw_bor /idx_bor_own. by iFrame. }
+  { rewrite /raw_bor /idx_bor_own. iExists j. by iFrame. }
   iSplitL "HB HκB Hbox".
   { rewrite /lft_bor_alive. iNext. iExists (<[j:=Bor_in]> B).
     rewrite /to_borUR !fmap_insert big_sepM_insert //. iFrame.
@@ -126,12 +128,12 @@ Proof.
   { rewrite /raw_bor /idx_bor_own /=. iFrame; auto. }
   iModIntro. rewrite -[S n]Nat.add_1_l -nat_op_plus auth_frag_op own_cnt_op.
   by iFrame.
-Admitted.
+Qed.
 
-Lemma raw_rebor E κ κ' i P :
+Lemma raw_rebor E κ κ' P :
   ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx -∗ raw_bor (κ, i) P ={E}=∗
-    ∃ j, raw_bor (κ', j) P ∗ ([†κ'] ={E}=∗ raw_bor (κ, i) P).
+  lft_ctx -∗ raw_bor κ P ={E}=∗
+    raw_bor κ' P ∗ ([†κ'] ={E}=∗ raw_bor κ P).
 Admitted.
 
 Lemma bor_rebor' E κ κ' P :