diff --git a/theories/lifetime/creation.v b/theories/lifetime/creation.v
index 26a83c554685bbcc429d164a05fb003fad57e099..44050811f14c74bf54b5b66c0374c81d4617d868 100644
--- a/theories/lifetime/creation.v
+++ b/theories/lifetime/creation.v
@@ -19,9 +19,9 @@ Proof.
   rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
 Qed.
 
-Lemma lft_vs_inv_frame (KI K : gset lft) κ :
+Lemma lft_inv_alive_acc (KI K : gset lft) κ :
   (∀ κ', κ' ∈ KI → κ' ⊂ κ → κ' ∈ K) →
-  ([∗ set] κ' ∈ K, lft_inv_alive κ') ⊢
+  ([∗ set] κ' ∈ K, lft_inv_alive κ') -∗
     ([∗ set] κ' ∈ KI, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ') ∗
     (([∗ set] κ' ∈ KI, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ') -∗
       ([∗ set] κ' ∈ K, lft_inv_alive κ')).
@@ -33,7 +33,7 @@ Proof.
 Qed.
 
 Lemma ilft_create A I κ :
-  own_ilft_auth I ⊢ own_alft_auth A -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
+  own_ilft_auth I -∗ own_alft_auth A -∗ ▷ ([∗ set] κ ∈ dom _ I, lft_inv A κ)
       ==∗ ∃ A' I', ⌜is_Some (I' !! κ)⌝ ∗
     own_ilft_auth I' ∗ own_alft_auth A' ∗ ▷ ([∗ set] κ ∈ dom _ I', lft_inv A' κ).
 Proof.
@@ -85,7 +85,7 @@ Proof.
     { rewrite /lft_inv. iNext. iRight. iSplit.
       { by iDestruct "Hdeadandalive" as "[? _]". }
       iPureIntro. exists Λ. rewrite lookup_insert; auto. }
-    iNext. iApply (big_sepS_impl _ _ (dom (gset lft) I) with "[$HA']").
+    iNext. iApply (@big_sepS_impl with "[$HA']").
     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.
@@ -106,7 +106,7 @@ Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
     ([∗ set] κ' ∈ K', lft_inv_dead κ'))%I in
   (∀ κ', is_Some (I !! κ') → κ' ⊂ κ → κ' ∈ K) →
   (∀ κ', is_Some (I !! κ') → κ ⊂ κ' → κ' ∈ K') →
-  Iinv ⊢ lft_inv_alive κ -∗ [†κ] ={⊤∖↑mgmtN}=∗ Iinv ∗ lft_inv_dead κ.
+  Iinv -∗ lft_inv_alive κ -∗ [†κ] ={⊤∖↑mgmtN}=∗ Iinv ∗ lft_inv_dead κ.
 Proof.
   iIntros (Iinv HK HK') "(HI & Halive & Hdead) Hlalive Hκ".
   rewrite lft_inv_alive_unfold;
@@ -119,14 +119,14 @@ Proof.
     { iDestruct (lft_tok_dead_own with "HB Hκ") as "[]". }
     iDestruct "HB" as "[% Hcnt]".
     iDestruct (own_cnt_auth with "HI Hcnt") as %?.
-    iDestruct (big_sepS_elem_of _ K' with "Hdead") as "Hdead"; first by eauto.
+    iDestruct (@big_sepS_elem_of with "Hdead") as "Hdead"; first by eauto.
     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.
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
-  iDestruct (lft_vs_inv_frame (dom _ I) _ κ with "Halive") as "[Halive Halive']".
+  iDestruct (lft_inv_alive_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.
@@ -147,7 +147,7 @@ Lemma lfts_kill A (I : gmap lft lft_names) (K K' : gset lft) :
   (∀ κ κ', κ ∈ K → is_Some (I !! κ') → κ ⊆ κ' → κ' ∈ K) →
   (∀ κ κ', κ ∈ K → lft_alive_in A κ → is_Some (I !! κ') →
     κ' ∉ K → κ' ⊂ κ → κ' ∈ K') →
-  Iinv K' ⊢ ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])
+  Iinv K' -∗ ([∗ set] κ ∈ K, lft_inv A κ ∗ [†κ])
     ={⊤∖↑mgmtN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
 Proof.
   intros Iinv. revert K'.
@@ -156,16 +156,15 @@ Proof.
   pose (Kalive := filter (lft_alive_in A) K).
   destruct (decide (Kalive = ∅)) as [HKalive|].
   { iModIntro. rewrite /Iinv. iFrame.
-    iApply (big_sepS_impl _ _ K with "[$HK]"); iAlways.
+    iApply (@big_sepS_impl with "[$HK]"); iAlways.
     rewrite /lft_inv. iIntros (κ Hκ) "[[[_ %]|[$ _]] _]". set_solver. }
   destruct (minimal_exists_L (⊂) Kalive)
     as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
-  iDestruct (big_sepS_delete _ K κ with "HK") as "[[Hκinv Hκ] HK]"; first done.
-  rewrite {1}/lft_inv. iDestruct "Hκinv" as "[[Hκalive _]|[_ %]]"; last first.
-  { by destruct (lft_alive_and_dead_in A κ). } 
+  iDestruct (@big_sepS_delete with "HK") as "[[Hκinv Hκ] HK]"; first done.
+  iDestruct (lft_inv_alive_in with "Hκinv") as "Hκalive"; first done.
   iAssert ⌜κ ∉ K'⌝%I with "[#]" as %HκK'.
   { iIntros (Hκ). iApply (lft_inv_alive_twice κ with "Hκalive").
-    by iApply (big_sepS_elem_of _ K' κ with "Halive"). }
+    by iApply (@big_sepS_elem_of with "Halive"). }
   specialize (IH (K ∖ {[ κ ]})). feed specialize IH; [set_solver +HκK|].
   iMod (IH ({[ κ ]} ∪ K') with "[HI Halive Hκalive] HK") as "[[HI Halive] Hdead]".
   { intros κ' κ''.
@@ -179,7 +178,7 @@ Proof.
        elem_of_union not_elem_of_singleton elem_of_singleton.
     intros [??] [?|?]; eauto. }
   { rewrite /Iinv big_sepS_insert //. iFrame. }
-  iDestruct (big_sepS_insert _ K' with "Halive") as "[Hκalive Halive]"; first done.
+  iDestruct (@big_sepS_insert with "Halive") as "[Hκalive Halive]"; first done.
   iMod (lft_kill with "[$HI $Halive $Hdead] Hκalive Hκ")
     as "[(HI&Halive&Hdead) Hκdead]".
   { intros κ' ??. eapply (HK' κ); eauto.
@@ -232,7 +231,7 @@ Proof.
   iMod ("Hclose" with "[HA HI Hinv]") as "_".
   { iNext. rewrite /lfts_inv /own_alft_auth.
     iExists (<[Λ:=true]>A), I; rewrite fmap_insert; iFrame.
-    iApply (big_sepS_impl _ _ (dom (gset lft) I) with "[$Hinv]").
+    iApply (@big_sepS_impl with "[$Hinv]").
     iAlways. rewrite /lft_inv. iIntros (κ ?) "[[Hκ %]|[Hκ %]]".
     - iLeft. iFrame "Hκ". iPureIntro. by apply lft_alive_in_insert.
     - iRight. iFrame "Hκ". iPureIntro. by apply lft_dead_in_insert. }
@@ -255,11 +254,11 @@ Proof.
   { apply union_least. apply kill_set_subseteq. apply down_close_subseteq. }
   rewrite HI !big_sepS_union //. iDestruct "Hinv" as "[[HinvK HinvD] Hinv]".
   iAssert ([∗ set] κ ∈ K', lft_inv_alive κ)%I with "[HinvD]" as "HinvD".
-  { iApply (big_sepS_impl _ _ K' with "[$HinvD]"); iIntros "!#".
-    rewrite /lft_inv. iIntros (κ Hκ) "[[$ _]|[_ %]]".
-    destruct (lft_alive_and_dead_in A κ); eauto using down_close_lft_alive_in. }
+  { iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
+    iIntros (κ Hκ) "?". iApply lft_inv_alive_in; last done.
+    eauto using down_close_lft_alive_in. }
   iAssert ([∗ set] κ ∈ K, lft_inv A κ ∗ [† κ])%I with "[HinvK]" as "HinvK". 
-  { iApply (big_sepS_impl _ _ K with "[$HinvK]"); iIntros "!#".
+  { iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
     iIntros (κ [? _]%elem_of_kill_set) "$". rewrite /lft_dead. eauto. }
   iMod (lfts_kill A I K K' with "[$HI $HinvD] HinvK") as "[[HI HinvD] HinvK]".
   { intros κ κ' [??]%elem_of_kill_set ??. apply elem_of_kill_set.
@@ -272,17 +271,17 @@ Proof.
   rewrite /own_alft_auth fmap_insert. iFrame "HA HI".
   rewrite HI !big_sepS_union //.
   iSplitL "HinvK HinvD"; first iSplitL "HinvK".
-  - iApply (big_sepS_impl _ _ K with "[$HinvK]"); iIntros "!#".
+  - iApply (@big_sepS_impl with "[$HinvK]"); iIntros "!#".
     iIntros (κ [? _]%elem_of_kill_set) "Hdead". rewrite /lft_inv.
     iRight. iFrame. iPureIntro. by apply lft_dead_in_insert_false'.
-  - iApply (big_sepS_impl _ _ K' with "[$HinvD]"); iIntros "!#".
+  - iApply (@big_sepS_impl with "[$HinvD]"); iIntros "!#".
     iIntros (κ Hκ) "Halive". rewrite /lft_inv.
     iLeft. iFrame "Halive". iPureIntro.
     assert (lft_alive_in A κ) as Halive by (by eapply down_close_lft_alive_in).
     apply lft_alive_in_insert_false; last done.
     apply elem_of_down_close in Hκ as (?&HFOO&_).
-    move: HFOO. by rewrite elem_of_kill_set not_and_l=> -[?|[] //].
-  - iApply (big_sepS_impl _ _ K'' with "[$Hinv]"); iIntros "!#".
+    move: HFOO. rewrite elem_of_kill_set. tauto.
+  - iApply (@big_sepS_impl with "[$Hinv]"); iIntros "!#".
     rewrite /lft_inv. iIntros (κ Hκ) "[[? %]|[? %]]".
     + iLeft. iFrame. iPureIntro.
       apply lft_alive_in_insert_false; last done.
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index c7c1a78e7ea786aa49d7084949e1886c823a74b1..86c44098e9a74f20ee689c11a221540b341fae66 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -3,6 +3,7 @@ From iris.prelude Require Export gmultiset strings.
 From iris.base_logic.lib Require Export invariants.
 From iris.base_logic.lib Require Import boxes.
 From iris.base_logic Require Import big_op.
+Import uPred.
 
 Definition lftN : namespace := nroot .@ "lft".
 Definition borN : namespace := lftN .@ "bor".
@@ -87,21 +88,21 @@ Section defs.
     | Bor_rebor κ' => ⌜κ ⊂ κ'⌝ ∗ own_cnt κ' (◯ 1)
     end%I.
 
-  Definition lft_bor_alive (κ : lft) (P : iProp Σ) : iProp Σ :=
+  Definition lft_bor_alive (κ : lft) (Pi : iProp Σ) : iProp Σ :=
     (∃ B : gmap slice_name bor_state,
-      box borN (bor_filled <$> B) P ∗
+      box borN (bor_filled <$> B) Pi ∗
       own_bor κ (● ((1%Qp,) ∘ DecAgree <$> B)) ∗
       [∗ map] s ∈ B, bor_cnt κ s)%I.
 
   Definition lft_bor_dead (κ : lft) : iProp Σ :=
-     (∃ (B: gset slice_name) (P : iProp Σ),
+     (∃ (B: gset slice_name) (Pb : iProp Σ),
        own_bor κ (● to_gmap (1%Qp, DecAgree Bor_in) B) ∗
-       box borN (to_gmap false B) P)%I.
+       box borN (to_gmap false B) Pb)%I.
 
-   Definition lft_inh (κ : lft) (s : bool) (P : iProp Σ) : iProp Σ :=
+   Definition lft_inh (κ : lft) (s : bool) (Pi : iProp Σ) : iProp Σ :=
      (∃ E : gset slice_name,
        own_inh κ (● GSet E) ∗
-       box inhN (to_gmap s E) P)%I.
+       box inhN (to_gmap s E) Pi)%I.
 
    Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
        (I : gmap lft lft_names) : iProp Σ :=
@@ -110,33 +111,33 @@ Section defs.
        [∗ set] κ' ∈ dom _ I, ∀ Hκ : κ' ⊂ κ, lft_inv_alive κ' Hκ)%I.
 
    Definition lft_vs_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
-       (P Q : iProp Σ) : iProp Σ :=
+       (Pb Pi : iProp Σ) : iProp Σ :=
      (∃ n : nat,
        own_cnt κ (● n) ∗
        ∀ I : gmap lft lft_names,
-         lft_vs_inv_go κ lft_inv_alive I -∗ ▷ P -∗ lft_dead κ
+         lft_vs_inv_go κ lft_inv_alive I -∗ ▷ Pb -∗ lft_dead κ
            ={⊤∖↑mgmtN}=∗
-         lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Q ∗ own_cnt κ (◯ n))%I.
+         lft_vs_inv_go κ lft_inv_alive I ∗ ▷ Pi ∗ own_cnt κ (◯ n))%I.
 
   Definition lft_inv_alive_go (κ : lft)
       (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ) : iProp Σ :=
-    (∃ P Q,
-      lft_bor_alive κ P ∗
-      lft_vs_go κ lft_inv_alive P Q ∗
-      lft_inh κ false Q)%I.
+    (∃ Pb Pi,
+      lft_bor_alive κ Pb ∗
+      lft_vs_go κ lft_inv_alive Pb Pi ∗
+      lft_inh κ false Pi)%I.
 
   Definition lft_inv_alive (κ : lft) : iProp Σ :=
     Fix_F _ lft_inv_alive_go (gmultiset_wf κ).
   Definition lft_vs_inv (κ : lft) (I : gmap lft lft_names) : iProp Σ :=
     lft_vs_inv_go κ (λ κ' _, lft_inv_alive κ') I.
-  Definition lft_vs (κ : lft) (P Q : iProp Σ) : iProp Σ :=
-    lft_vs_go κ (λ κ' _, lft_inv_alive κ') P Q.
+  Definition lft_vs (κ : lft) (Pb Pi : iProp Σ) : iProp Σ :=
+    lft_vs_go κ (λ κ' _, lft_inv_alive κ') Pb Pi.
 
   Definition lft_inv_dead (κ : lft) : iProp Σ :=
-    (∃ P,
+    (∃ Pi,
       lft_bor_dead κ ∗
       own_cnt κ (● 0) ∗
-      lft_inh κ true P)%I.
+      lft_inh κ true Pi)%I.
 
   Definition lft_alive_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
     ∀ Λ:atomic_lft, Λ ∈ κ → A !! Λ = Some true.
@@ -193,3 +194,106 @@ Infix "⊑" := lft_incl (at level 70) : uPred_scope.
 Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   lft_inh lft_inv_alive lft_vs_inv lft_vs lft_inv_dead lft_inv lft_incl
   idx_bor_own idx_bor raw_bor bor.
+
+Section basic_properties.
+Context `{invG Σ, lftG Σ}.
+Implicit Types κ : lft.
+
+(* Unfolding lemmas *)
+Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) I n :
+  (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
+  lft_vs_inv_go κ f I ≡{n}≡ lft_vs_inv_go κ f' I.
+Proof.
+  intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ'.
+  by apply forall_ne=> Hκ.
+Qed.
+
+Lemma lft_vs_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) Pb Pb' Pi Pi' n :
+  (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
+  Pb ≡{n}≡ Pb' → Pi ≡{n}≡ Pi' →
+  lft_vs_go κ f Pb Pi ≡{n}≡ lft_vs_go κ f' Pb' Pi'.
+Proof.
+  intros Hf HPb HPi. apply exist_ne=> n'.
+  apply sep_ne, forall_ne=> // I. rewrite lft_vs_inv_go_ne //. solve_proper.
+Qed.
+
+Lemma lft_inv_alive_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) n :
+  (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
+  lft_inv_alive_go κ f ≡{n}≡ lft_inv_alive_go κ f'.
+Proof.
+  intros Hf. apply exist_ne=> Pb; apply exist_ne=> Pi. by rewrite lft_vs_go_ne.
+Qed.
+
+Lemma lft_inv_alive_unfold κ :
+  lft_inv_alive κ ⊣⊢ ∃ Pb Pi,
+    lft_bor_alive κ Pb ∗ lft_vs κ Pb Pi ∗ lft_inh κ false Pi.
+Proof.
+  apply equiv_dist=> n. rewrite /lft_inv_alive -Fix_F_eq.
+  apply lft_inv_alive_go_ne=> κ' Hκ.
+  apply (Fix_F_proper _ (λ _, dist n)); auto using lft_inv_alive_go_ne.
+Qed.
+Lemma lft_vs_inv_unfold κ (I : gmap lft lft_names) :
+  lft_vs_inv κ I ⊣⊢ lft_bor_dead κ ∗
+    own_ilft_auth I ∗
+    [∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ'.
+Proof.
+  rewrite /lft_vs_inv /lft_vs_inv_go. by setoid_rewrite pure_impl_forall.
+Qed.
+Lemma lft_vs_unfold κ Pb Pi :
+  lft_vs κ Pb Pi ⊣⊢ ∃ n : nat,
+    own_cnt κ (● n) ∗
+    ∀ I : gmap lft lft_names,
+      lft_vs_inv κ I -∗ ▷ Pb -∗ lft_dead κ ={⊤∖↑mgmtN}=∗
+      lft_vs_inv κ I ∗ ▷ Pi ∗ own_cnt κ (◯ n).
+Proof. done. Qed.
+
+Global Instance lft_bor_alive_ne κ n : Proper (dist n ==> dist n) (lft_bor_alive κ).
+Proof. solve_proper. Qed.
+Global Instance lft_bor_alive_proper κ : Proper ((≡) ==> (≡)) (lft_bor_alive κ).
+Proof. apply (ne_proper _). Qed.
+
+Global Instance lft_inh_ne κ s n : Proper (dist n ==> dist n) (lft_inh κ s).
+Proof. solve_proper. Qed.
+Global Instance lft_inh_proper κ s : Proper ((≡) ==> (≡)) (lft_inh κ s).
+Proof. apply (ne_proper _). Qed.
+
+Global Instance lft_vs_ne κ n :
+  Proper (dist n ==> dist n ==> dist n) (lft_vs κ).
+Proof. intros P P' HP Q Q' HQ. by apply lft_vs_go_ne. Qed.
+Global Instance lft_vs_proper κ : Proper ((≡) ==> (≡) ==> (≡)) (lft_vs κ).
+Proof. apply (ne_proper_2 _). Qed.
+
+Global Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
+Proof. solve_proper. Qed.
+Global Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
+Proof. apply (ne_proper _). Qed.
+
+Global Instance raw_bor_ne i n : Proper (dist n ==> dist n) (raw_bor i).
+Proof. solve_proper. Qed.
+Global Instance raw_bor_proper i : Proper ((≡) ==> (≡)) (raw_bor i).
+Proof. apply (ne_proper _). Qed.
+
+Global Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
+Proof. solve_proper. Qed.
+Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
+Proof. apply (ne_proper _). Qed.
+
+(*** PersistentP and TimelessP instances  *)
+Global Instance lft_tok_timeless q κ : TimelessP q.[κ].
+Proof. rewrite /lft_tok. apply _. Qed.
+Global Instance lft_dead_persistent κ : PersistentP [†κ].
+Proof. rewrite /lft_dead. apply _. Qed.
+Global Instance lft_dead_timeless κ : PersistentP [†κ].
+Proof. rewrite /lft_tok. apply _. Qed.
+
+Global Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
+Proof. rewrite /lft_incl. apply _. Qed.
+
+Global Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
+Proof. rewrite /idx_bor. apply _. Qed.
+Global Instance idx_borrow_own_timeless q i : TimelessP (idx_bor_own q i).
+Proof. rewrite /idx_bor_own. apply _. Qed.
+
+Global Instance lft_ctx_persistent : PersistentP lft_ctx.
+Proof. rewrite /lft_ctx. apply _. Qed.
+End basic_properties.
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 60a9a34cae254240bf5c109fe0e04755b0f68925..1ad2a063f82e5cf9ab62a7b8dffda85222bac06e 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -8,167 +8,7 @@ Section primitive.
 Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
-(* Unfolding lemmas *)
-Lemma lft_vs_inv_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) I n :
-  (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
-  lft_vs_inv_go κ f I ≡{n}≡ lft_vs_inv_go κ f' I.
-Proof.
-  intros Hf. apply sep_ne, sep_ne, big_opS_ne=> // κ'.
-  by apply forall_ne=> Hκ.
-Qed.
-
-Lemma lft_vs_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) P P' Q Q' n :
-  (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
-  P ≡{n}≡ P' → Q ≡{n}≡ Q' →
-  lft_vs_go κ f P Q ≡{n}≡ lft_vs_go κ f' P' Q'.
-Proof.
-  intros Hf HP HQ. apply exist_ne=> n'.
-  apply sep_ne, forall_ne=> // I. rewrite lft_vs_inv_go_ne //. solve_proper.
-Qed.
-
-Lemma lft_inv_alive_go_ne κ (f f' : ∀ κ', κ' ⊂ κ → iProp Σ) n :
-  (∀ κ' (Hκ : κ' ⊂ κ), f κ' Hκ ≡{n}≡ f' κ' Hκ) →
-  lft_inv_alive_go κ f ≡{n}≡ lft_inv_alive_go κ f'.
-Proof.
-  intros Hf. apply exist_ne=> P; apply exist_ne=> Q. by rewrite lft_vs_go_ne.
-Qed.
-
-Lemma lft_inv_alive_unfold κ :
-  lft_inv_alive κ ⊣⊢ ∃ P Q, lft_bor_alive κ P ∗ lft_vs κ P Q ∗ lft_inh κ false Q.
-Proof.
-  apply equiv_dist=> n. rewrite /lft_inv_alive -Fix_F_eq.
-  apply lft_inv_alive_go_ne=> κ' Hκ.
-  apply (Fix_F_proper _ (λ _, dist n)); auto using lft_inv_alive_go_ne.
-Qed.
-Lemma lft_vs_inv_unfold κ (I : gmap lft lft_names) :
-  lft_vs_inv κ I ⊣⊢ lft_bor_dead κ ∗
-    own_ilft_auth I ∗
-    [∗ set] κ' ∈ dom _ I, ⌜κ' ⊂ κ⌝ → lft_inv_alive κ'.
-Proof.
-  rewrite /lft_vs_inv /lft_vs_inv_go. by setoid_rewrite pure_impl_forall.
-Qed.
-Lemma lft_vs_unfold κ P Q :
-  lft_vs κ P Q ⊣⊢ ∃ n : nat,
-    own_cnt κ (● n) ∗
-    ∀ I : gmap lft lft_names,
-      lft_vs_inv κ I -∗ ▷ P -∗ lft_dead κ ={⊤∖↑mgmtN}=∗
-      lft_vs_inv κ I ∗ ▷ Q ∗ own_cnt κ (◯ n).
-Proof. done. Qed.
-
-Global Instance lft_bor_alive_ne κ n : Proper (dist n ==> dist n) (lft_bor_alive κ).
-Proof. solve_proper. Qed.
-Global Instance lft_bor_alive_proper κ : Proper ((≡) ==> (≡)) (lft_bor_alive κ).
-Proof. apply (ne_proper _). Qed.
-
-Global Instance lft_inh_ne κ s n : Proper (dist n ==> dist n) (lft_inh κ s).
-Proof. solve_proper. Qed.
-Global Instance lft_inh_proper κ s : Proper ((≡) ==> (≡)) (lft_inh κ s).
-Proof. apply (ne_proper _). Qed.
-
-Global Instance lft_vs_ne κ n :
-  Proper (dist n ==> dist n ==> dist n) (lft_vs κ).
-Proof. intros P P' HP Q Q' HQ. by apply lft_vs_go_ne. Qed.
-Global Instance lft_vs_proper κ : Proper ((≡) ==> (≡) ==> (≡)) (lft_vs κ).
-Proof. apply (ne_proper_2 _). Qed.
-
-Global Instance idx_bor_ne κ i n : Proper (dist n ==> dist n) (idx_bor κ i).
-Proof. solve_proper. Qed.
-Global Instance idx_bor_proper κ i : Proper ((≡) ==> (≡)) (idx_bor κ i).
-Proof. apply (ne_proper _). Qed.
-
-Global Instance raw_bor_ne i n : Proper (dist n ==> dist n) (raw_bor i).
-Proof. solve_proper. Qed.
-Global Instance raw_bor_proper i : Proper ((≡) ==> (≡)) (raw_bor i).
-Proof. apply (ne_proper _). Qed.
-
-Global Instance bor_ne κ n : Proper (dist n ==> dist n) (bor κ).
-Proof. solve_proper. Qed.
-Global Instance bor_proper κ : Proper ((≡) ==> (≡)) (bor κ).
-Proof. apply (ne_proper _). Qed.
-
-(*** PersistentP and TimelessP instances  *)
-Global Instance lft_tok_timeless q κ : TimelessP q.[κ].
-Proof. rewrite /lft_tok. apply _. Qed.
-Global Instance lft_dead_persistent κ : PersistentP [†κ].
-Proof. rewrite /lft_dead. apply _. Qed.
-Global Instance lft_dead_timeless κ : PersistentP [†κ].
-Proof. rewrite /lft_tok. apply _. Qed.
-
-Global Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
-Proof. rewrite /lft_incl. apply _. Qed.
-
-Global Instance idx_bor_persistent κ i P : PersistentP (&{κ,i} P).
-Proof. rewrite /idx_bor. apply _. Qed.
-Global Instance idx_borrow_own_timeless q i : TimelessP (idx_bor_own q i).
-Proof. rewrite /idx_bor_own. apply _. Qed.
-
-Global Instance lft_ctx_persistent : PersistentP lft_ctx.
-Proof. rewrite /lft_ctx. apply _. Qed.
-
-(** Alive and dead *)
-Global Instance lft_alive_in_dec A κ : Decision (lft_alive_in A κ).
-Proof.
-  refine (cast_if (decide (set_Forall (λ Λ, A !! Λ = Some true)
-                  (dom (gset atomic_lft) κ))));
-    rewrite /lft_alive_in; by setoid_rewrite <-gmultiset_elem_of_dom.
-Qed.
-Global Instance lft_dead_in_dec A κ : Decision (lft_dead_in A κ).
-Proof.
-  refine (cast_if (decide (set_Exists (λ Λ, A !! Λ = Some false)
-                  (dom (gset atomic_lft) κ))));
-      rewrite /lft_dead_in; by setoid_rewrite <-gmultiset_elem_of_dom.
-Qed.
-
-Lemma lft_alive_or_dead_in A κ :
-  (∃ Λ, Λ ∈ κ ∧ A !! Λ = None) ∨ (lft_alive_in A κ ∨ lft_dead_in A κ).
-Proof.
-  rewrite /lft_alive_in /lft_dead_in.
-  destruct (decide (set_Exists (λ Λ, A !! Λ = None) (dom (gset _) κ)))
-    as [(Λ & ?%gmultiset_elem_of_dom & HAΛ)|HA%(not_set_Exists_Forall _)]; first eauto.
-  destruct (decide (set_Exists (λ Λ, A !! Λ = Some false) (dom (gset _) κ)))
-    as [(Λ & HΛ%gmultiset_elem_of_dom & ?)|HA'%(not_set_Exists_Forall _)]; first eauto.
-  right; left. intros Λ HΛ%gmultiset_elem_of_dom.
-  move: (HA _ HΛ) (HA' _ HΛ)=> /=. case: (A !! Λ)=>[[]|]; naive_solver.
-Qed.
-Lemma lft_alive_and_dead_in A κ : lft_alive_in A κ → lft_dead_in A κ → False.
-Proof. intros Halive (Λ&HΛ&?). generalize (Halive _ HΛ). naive_solver. Qed.
-
-Lemma lft_alive_in_subseteq A κ κ' :
-  lft_alive_in A κ → κ' ⊆ κ → lft_alive_in A κ'.
-Proof. intros Halive ? Λ ?. by eapply Halive, gmultiset_elem_of_subseteq. Qed.
-
-Lemma lft_alive_in_insert A κ Λ b :
-  A !! Λ = None → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
-Proof.
-  intros HΛ Halive Λ' HΛ'.
-  assert (Λ ≠ Λ') by (intros ->; move:(Halive _ HΛ'); by rewrite HΛ).
-  rewrite lookup_insert_ne; eauto.
-Qed.
-Lemma lft_alive_in_insert_false A κ Λ b :
-  Λ ∉ κ → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
-Proof.
-  intros HΛ Halive Λ' HΛ'.
-  rewrite lookup_insert_ne; last (by intros ->); auto.
-Qed.
-
-Lemma lft_dead_in_insert A κ Λ b :
-  A !! Λ = None → lft_dead_in A κ → lft_dead_in (<[Λ:=b]> A) κ.
-Proof.
-  intros HΛ (Λ'&?&HΛ').
-  assert (Λ ≠ Λ') by (intros ->; move:HΛ'; by rewrite HΛ).
-  exists Λ'. by rewrite lookup_insert_ne.
-Qed.
-Lemma lft_dead_in_insert_false A κ Λ :
-  lft_dead_in A κ → lft_dead_in (<[Λ:=false]> A) κ.
-Proof.
-  intros (Λ'&?&HΛ'). destruct (decide (Λ = Λ')) as [<-|].
-  - exists Λ. by rewrite lookup_insert.
-  - exists Λ'. by rewrite lookup_insert_ne.
-Qed.
-Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
-Proof. exists Λ. by rewrite lookup_insert. Qed.
-
-(** Silly stuff *)
+(** Ownership *)
 Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
   own_ilft_auth I ⊢
     own ilft_name (◯ {[κ := DecAgree γs]}) -∗ ⌜is_Some (I !! κ)⌝.
@@ -267,6 +107,69 @@ Proof.
   iDestruct 1 as (γs) "[#Hκ Hx]"; iExists γs. iFrame "Hκ". by iApply own_update.
 Qed.
 
+(** Alive and dead *)
+Global Instance lft_alive_in_dec A κ : Decision (lft_alive_in A κ).
+Proof.
+  refine (cast_if (decide (set_Forall (λ Λ, A !! Λ = Some true)
+                  (dom (gset atomic_lft) κ))));
+    rewrite /lft_alive_in; by setoid_rewrite <-gmultiset_elem_of_dom.
+Qed.
+Global Instance lft_dead_in_dec A κ : Decision (lft_dead_in A κ).
+Proof.
+  refine (cast_if (decide (set_Exists (λ Λ, A !! Λ = Some false)
+                  (dom (gset atomic_lft) κ))));
+      rewrite /lft_dead_in; by setoid_rewrite <-gmultiset_elem_of_dom.
+Qed.
+
+Lemma lft_alive_or_dead_in A κ :
+  (∃ Λ, Λ ∈ κ ∧ A !! Λ = None) ∨ (lft_alive_in A κ ∨ lft_dead_in A κ).
+Proof.
+  rewrite /lft_alive_in /lft_dead_in.
+  destruct (decide (set_Exists (λ Λ, A !! Λ = None) (dom (gset _) κ)))
+    as [(Λ & ?%gmultiset_elem_of_dom & HAΛ)|HA%(not_set_Exists_Forall _)]; first eauto.
+  destruct (decide (set_Exists (λ Λ, A !! Λ = Some false) (dom (gset _) κ)))
+    as [(Λ & HΛ%gmultiset_elem_of_dom & ?)|HA'%(not_set_Exists_Forall _)]; first eauto.
+  right; left. intros Λ HΛ%gmultiset_elem_of_dom.
+  move: (HA _ HΛ) (HA' _ HΛ)=> /=. case: (A !! Λ)=>[[]|]; naive_solver.
+Qed.
+Lemma lft_alive_and_dead_in A κ : lft_alive_in A κ → lft_dead_in A κ → False.
+Proof. intros Halive (Λ&HΛ&?). generalize (Halive _ HΛ). naive_solver. Qed.
+
+Lemma lft_alive_in_subseteq A κ κ' :
+  lft_alive_in A κ → κ' ⊆ κ → lft_alive_in A κ'.
+Proof. intros Halive ? Λ ?. by eapply Halive, gmultiset_elem_of_subseteq. Qed.
+
+Lemma lft_alive_in_insert A κ Λ b :
+  A !! Λ = None → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
+Proof.
+  intros HΛ Halive Λ' HΛ'.
+  assert (Λ ≠ Λ') by (intros ->; move:(Halive _ HΛ'); by rewrite HΛ).
+  rewrite lookup_insert_ne; eauto.
+Qed.
+Lemma lft_alive_in_insert_false A κ Λ b :
+  Λ ∉ κ → lft_alive_in A κ → lft_alive_in (<[Λ:=b]> A) κ.
+Proof.
+  intros HΛ Halive Λ' HΛ'.
+  rewrite lookup_insert_ne; last (by intros ->); auto.
+Qed.
+
+Lemma lft_dead_in_insert A κ Λ b :
+  A !! Λ = None → lft_dead_in A κ → lft_dead_in (<[Λ:=b]> A) κ.
+Proof.
+  intros HΛ (Λ'&?&HΛ').
+  assert (Λ ≠ Λ') by (intros ->; move:HΛ'; by rewrite HΛ).
+  exists Λ'. by rewrite lookup_insert_ne.
+Qed.
+Lemma lft_dead_in_insert_false A κ Λ :
+  lft_dead_in A κ → lft_dead_in (<[Λ:=false]> A) κ.
+Proof.
+  intros (Λ'&?&HΛ'). destruct (decide (Λ = Λ')) as [<-|].
+  - exists Λ. by rewrite lookup_insert.
+  - exists Λ'. by rewrite lookup_insert_ne.
+Qed.
+Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
+Proof. exists Λ. by rewrite lookup_insert. Qed.
+
 Lemma lft_inv_alive_twice κ : lft_inv_alive κ ⊢ lft_inv_alive κ -∗ False.
 Proof.
   rewrite lft_inv_alive_unfold /lft_inh.
@@ -275,6 +178,17 @@ Proof.
   by iDestruct (own_inh_valid_2 with "HE HE'") as %?.
 Qed.
 
+Lemma lft_inv_alive_in A κ : lft_alive_in A κ → lft_inv A κ -∗ lft_inv_alive κ.
+Proof.
+  rewrite /lft_inv. iIntros (?) "[[$ _]|[_ %]]".
+  by destruct (lft_alive_and_dead_in A κ).
+Qed.
+Lemma lft_inv_dead_in A κ : lft_dead_in A κ → lft_inv A κ -∗ lft_inv_dead κ.
+Proof.
+  rewrite /lft_inv. iIntros (?) "[[_ %]|[$ _]]".
+  by destruct (lft_alive_and_dead_in A κ).
+Qed.
+
 (** Basic rules about lifetimes  *)
 Lemma lft_tok_op q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
 Proof. by rewrite /lft_tok -big_sepMS_union. Qed.
diff --git a/theories/lifetime/rebor.v b/theories/lifetime/rebor.v
new file mode 100644
index 0000000000000000000000000000000000000000..0ed3c79deba9d53743cbd8831a879f01ffa12cf6
--- /dev/null
+++ b/theories/lifetime/rebor.v
@@ -0,0 +1,64 @@
+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 rebor.
+Context `{invG Σ, lftG Σ}.
+Implicit Types κ : lft.
+
+Lemma bor_fake E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
+Proof.
+Admitted.
+
+Lemma raw_bor_unnest A I Pb Pi P κ κ' i :
+  let Iinv := (
+    own_ilft_auth I ∗
+    ▷ ([∗ set] κ ∈ dom _ I ∖ {[ κ' ]}, lft_inv A κ) ∗
+    ▷ lft_bor_alive κ' Pb)%I in
+  κ ⊆ κ' →
+  lft_alive_in A κ' →
+  Iinv -∗ raw_bor (κ,i) P -∗ ▷ lft_vs κ' (Pb ∗ raw_bor (κ,i) P) Pi ={↑borN}=∗
+    ∃ Pb' j, Iinv ∗ raw_bor (κ',j) P ∗ ▷ lft_vs κ' Pb' Pi.
+Proof.
+  iIntros (Iinv Hκκ' Haliveκ') "(HI & HA & Hbor) Hraw Hvs".
+  destruct (decide (κ = κ')) as [<-|Hκneq].
+  { 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 "[Hraw Hslice]".
+  iDestruct (own_bor_auth with "HI Hraw") as %?.
+  rewrite big_sepS_later.
+  iDestruct (big_sepS_elem_of_acc _ (dom (gset lft) I ∖ _) κ
+    with "HA") as "[HAκ HA]".
+  { by rewrite elem_of_difference elem_of_dom not_elem_of_singleton. }
+  rewrite {1}/lft_inv. iDestruct "HAκ" as "[[HAκ >%]|[_ >%]]"; last first.
+  { destruct (lft_alive_and_dead_in A κ); eauto using lft_alive_in_subseteq. }
+  rewrite lft_inv_alive_unfold;
+    iDestruct "HAκ" as (Pb' Pi') "(Hbor'&Hvs'&Hinh')".
+  rewrite {2}/lft_bor_alive; iDestruct "Hbor'" as (B) "(Hbox & >HκB & HB)".
+  iDestruct (own_bor_valid_2 with "HκB Hraw") as %[HB _]%auth_valid_discrete_2.
+  move: HB=> /singleton_included=> -[qs].
+  rewrite leibniz_equiv_iff lookup_fmap fmap_Some=> -[[s [? ->]] /Some_pair_included [??]].
+SearchAbout Some included.
+  apply singleton_included in HB as (?&?&?).
+SearchAbout 
+simpl in *.
+  
+  Check big_sepS_delete.
+Admitted.
+
+Lemma bor_rebor' E κ κ' P :
+  ↑lftN ⊆ E → κ ⊆ κ' →
+  lft_ctx ⊢ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
+Proof. Admitted.
+Lemma bor_unnest E κ κ' P :
+  ↑lftN ⊆ E →
+  lft_ctx ⊢ &{κ'} &{κ} P ={E}▷=∗ &{κ ∪ κ'} P.
+Proof. Admitted.
\ No newline at end of file
diff --git a/theories/lifetime/todo.v b/theories/lifetime/todo.v
index ce6374f9e36a2312584354497d73431150106bb9..5d60fea4af1e9eee093c6268f1191cfbd7f30ede 100644
--- a/theories/lifetime/todo.v
+++ b/theories/lifetime/todo.v
@@ -25,14 +25,6 @@ Lemma bor_acc_atomic_strong E κ P :
     (▷ P ∗ ∀ Q, ▷ Q ∗ ▷ ([†κ] -∗ ▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
     [†κ] ∗ |={E∖↑lftN,E}=> True.
 Proof. Admitted.
-Lemma bor_reborrow' E κ κ' P :
-  ↑lftN ⊆ E → κ ⊆ κ' →
-  lft_ctx ⊢ &{κ} P ={E}=∗ &{κ'} P ∗ ([†κ'] ={E}=∗ &{κ} P).
-Proof. Admitted.
-Lemma bor_unnest E κ κ' P :
-  ↑lftN ⊆ E →
-  lft_ctx ⊢ &{κ'} &{κ} P ={E}▷=∗ &{κ ∪ κ'} P.
-Proof. Admitted.
 
 (** Indexed borrow *)
 Lemma idx_bor_acc E q κ i P :