Stuck.

theories/lifetime/primitive.v

@@ -302,6 +302,16 @@ Proof.
   - rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
 Qed.
 
+Lemma lft_incl_mono κ1 κ1' κ2 κ2' :
+  κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
+Proof.
+  iIntros "#H1 #H2". iApply (lft_incl_glb with "[]").
+  - iApply (lft_incl_trans with "[] H1").
+    iApply lft_le_incl. apply gmultiset_union_subseteq_l.
+  - iApply (lft_incl_trans with "[] H2").
+    iApply lft_le_incl. apply gmultiset_union_subseteq_r.
+Qed.
+
 Lemma lft_incl_acc E κ κ' q :
   ↑lftN ⊆ E →
   κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).

theories/lifetime/raw_reborrow.v

@@ -129,7 +129,7 @@ Proof.
   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. }
+  { by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
   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|..].

theories/lifetime/reborrow.v

-From lrust.lifetime Require Export derived.
-From lrust.lifetime Require Export raw_reborrow.
+From lrust.lifetime Require Export borrow derived.
+From lrust.lifetime Require Import 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.
 From iris.proofmode Require Import tactics.
@@ -28,13 +29,38 @@ Lemma bor_unnest E κ κ' P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
 Proof.
-  iIntros (?) "#LFT Hκ'". rewrite {2}/bor.
-  iMod (bor_exists with "LFT Hκ'") as (κ'') "Hκ'"; first done.
-  rewrite {1}/bor; iDestruct "Hκ'" as (κ''') "[#H⊑' Hκ''']".
-(*
-  iMod (raw_rebor _ _ (κ'' ∪ κ''') with "LFT Hκ'''") as "[Hκ Hclose]"; first done.
+  iIntros (?) "#LFT Hκ". rewrite {2}/bor.
+  iMod (bor_exists with "LFT Hκ") as (κ0) "Hκ"; first done.
+  rewrite {1}/bor; iDestruct "Hκ" as (κ0') "[#H⊑ Hκ]".
+  set (κ'' := κ0 ∪ κ0').
+  iMod (raw_rebor _ _ κ'' with "LFT Hκ") as "[Hκ _]"; first done.
   { apply gmultiset_union_subseteq_r. }
-Check   
-Qed. *)
+  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 "[Hinv' Hinv]";
+    first by apply elem_of_dom.
+  rewrite {1}/lft_inv; iDestruct "Hinv'" as "[[Hinv' >%]|[Hdead >%]]"; last first.
+  { rewrite /lft_inv_dead;
+      iDestruct "Hdead" as (Pi) "(Hdead & Hcnt & Hinh)".
+    iMod (raw_bor_fake _ true _ P with "Hdead")
+      as "[Hdead Hbor]"; first solve_ndisj.
+    iMod ("Hclose" with "[- Hbor]") 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; last auto.
+      rewrite /lft_inv_dead. iExists Pi. iFrame. }
+    iApply (step_fupd_mask_mono E _ _ E); try solve_ndisj.
+    rewrite /bor. do 3 iModIntro. 
+    iExists κ''. iFrame "Hbor". rewrite /κ''.
+    (* Why is this going to work out *)
+    admit. }
+  rewrite {1}/raw_bor /idx_bor_own /=; iDestruct "Hκ" as (i) "[Hi #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 (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
 Admitted.
 End reborrow.