diff --git a/_CoqProject b/_CoqProject
index d8ed7fbb138be4f221611e7d7f8ed9c9b9ab0a7c..c64653019cc75e03e59e33475feaf8b2b19c7fd0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,3 +5,4 @@ theories/lifetime/derived.v
 theories/lifetime/creation.v
 theories/lifetime/primitive.v
 theories/lifetime/todo.v
+theories/lifetime/borrow.v
diff --git a/iris b/iris
index 020acf846aaf5fa367761cff22e7b74160ddc4b0..ff96075aa1472b1c3b0cfee87cc4ffb06e0f1e2b 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit 020acf846aaf5fa367761cff22e7b74160ddc4b0
+Subproject commit ff96075aa1472b1c3b0cfee87cc4ffb06e0f1e2b
diff --git a/theories/lifetime/definitions.v b/theories/lifetime/definitions.v
index 41f14673fe79760a70f8994a696816dd0ded35e1..c7c1a78e7ea786aa49d7084949e1886c823a74b1 100644
--- a/theories/lifetime/definitions.v
+++ b/theories/lifetime/definitions.v
@@ -27,6 +27,9 @@ Definition lft_stateR := csumR fracR unitR.
 Definition to_lft_stateR (b : bool) : lft_stateR :=
   if b then Cinl 1%Qp else Cinr ().
 
+Instance to_lft_stateR_inj : Inj eq eq to_lft_stateR.
+Proof. by intros [] []. Qed.
+
 Record lft_names := LftNames {
   bor_name : gname;
   cnt_name : gname;
@@ -136,9 +139,9 @@ Section defs.
       lft_inh κ true P)%I.
 
   Definition lft_alive_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
-    ∀ Λ, Λ ∈ κ → A !! Λ = Some true.
+    ∀ Λ:atomic_lft, Λ ∈ κ → A !! Λ = Some true.
   Definition lft_dead_in (A : gmap atomic_lft bool) (κ : lft) : Prop :=
-    ∃ Λ, Λ ∈ κ ∧ A !! Λ = Some false.
+    ∃ Λ:atomic_lft, Λ ∈ κ ∧ A !! Λ = Some false.
 
   Definition lft_inv (A : gmap atomic_lft bool) (κ : lft) : iProp Σ :=
     (lft_inv_alive κ ∗ ⌜lft_alive_in A κ⌝ ∨
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index d0aca0a09f31f18a55ab1c6b4e697cd1951e074e..6cd9289f6ad55fd89bf3c5f051c33b448ba54529 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -1,4 +1,4 @@
-From lrust.lifetime Require Export primitive todo.
+From lrust.lifetime Require Export primitive borrow todo.
 From iris.proofmode Require Import tactics.
 
 Section derived.
@@ -59,27 +59,6 @@ Proof.
   iIntros (?) "#[_ H] Hq". iApply fupd_mask_mono; first done. by iApply "H".
 Qed.
 
-Lemma lft_le_incl κ κ' : κ' ⊆ κ → True ⊢ κ ⊑ κ'.
-Proof. (*
-  iIntros (->%gmultiset_union_difference) "!#". iSplitR.
-  - iIntros (q). rewrite -lft_tok_op. iIntros (q) "[Hκ' Hκ0]". iExists q. iIntros "!>{$Hκ'}Hκ'!>". by iSplitR "Hκ0".
-  - iIntros "? !>". iApply lft_dead_or. auto.
-Qed. *) Admitted.
-
-Lemma lft_incl_refl κ : True ⊢ κ ⊑ κ.
-Proof. by apply lft_le_incl. Qed.
-
-Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
-Proof.
-  rewrite /lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]] !#". iSplitR.
-  - iIntros (q) "Hκ".
-    iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
-    iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
-    iExists q''. iIntros "{$Hκ''} !> Hκ''".
-    iMod ("Hclose'" with "Hκ''") as "Hκ'". by iApply "Hclose".
-  - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
-Qed.
-
 Lemma bor_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -∗ &{κ}P.
 Proof.
   iIntros "Hκκ' H". rewrite /bor. iDestruct "H" as (i) "[??]".
diff --git a/theories/lifetime/primitive.v b/theories/lifetime/primitive.v
index 27fb4938c3d9f27f7556014371a83221ccaa473c..60a9a34cae254240bf5c109fe0e04755b0f68925 100644
--- a/theories/lifetime/primitive.v
+++ b/theories/lifetime/primitive.v
@@ -178,6 +178,18 @@ Proof.
   simplify_map_eq; simplify_option_eq; eauto.
 Qed.
 
+Lemma own_alft_auth_agree (A : gmap atomic_lft bool) Λ b :
+  own_alft_auth A ⊢
+    own alft_name (◯ {[Λ := to_lft_stateR b]}) -∗ ⌜A !! Λ = Some b⌝.
+Proof.
+  iIntros "HA HΛ". iDestruct (own_valid_2 with "HA HΛ")
+    as %[[? [Heq Hle]]%singleton_included _]%auth_valid_discrete_2.
+  simplify_map_eq. destruct (A!!Λ) as [b'|]; last done. inversion Heq. subst x.
+  apply Some_included in Hle. destruct Hle as [->%leibniz_equiv%(inj _)|Hle]. done.
+  apply csum_included in Hle.
+  destruct Hle as [Hle|[(?&?&?&?&?)|(?&?&?&?&?)]], b, b'; try done.
+Qed.
+
 Lemma own_bor_auth I κ x : own_ilft_auth I ⊢ own_bor κ x -∗ ⌜is_Some (I !! κ)⌝.
 Proof.
   iIntros "HI"; iDestruct 1 as (γs) "[? _]".
@@ -295,4 +307,27 @@ Proof. by rewrite /lft_tok big_sepMS_empty. Qed.
 
 Lemma lft_dead_static : [† static] ⊢ False.
 Proof. rewrite /lft_dead. iDestruct 1 as (Λ) "[% H']". set_solver. Qed.
+
+Lemma lft_le_incl κ κ' : κ' ⊆ κ → True ⊢ κ ⊑ κ'.
+Proof.
+  iIntros (->%gmultiset_union_difference) "!#". iSplitR.
+  - iIntros (q). rewrite <-lft_tok_op. iIntros "[H Hf]". iExists q. iFrame.
+    rewrite <-lft_tok_op. by iIntros "!>{$Hf}$".
+  - iIntros "? !>". iApply lft_dead_or. auto.
+Qed.
+
+Lemma lft_incl_refl κ : True ⊢ κ ⊑ κ.
+Proof. by apply lft_le_incl. Qed.
+
+Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
+Proof.
+  rewrite /lft_incl. iIntros "[#[H1 H1†] #[H2 H2†]] !#". iSplitR.
+  - iIntros (q) "Hκ".
+    iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
+    iMod ("H2" with "*Hκ'") as (q'') "[Hκ'' Hclose']".
+    iExists q''. iIntros "{$Hκ''} !> Hκ''".
+    iMod ("Hclose'" with "Hκ''") as "Hκ'". by iApply "Hclose".
+  - iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
+Qed.
+
 End primitive.
diff --git a/theories/lifetime/todo.v b/theories/lifetime/todo.v
index 6d19e3e62184bcda33a1a29ceb8c38a6476f2baa..ce6374f9e36a2312584354497d73431150106bb9 100644
--- a/theories/lifetime/todo.v
+++ b/theories/lifetime/todo.v
@@ -5,15 +5,6 @@ Context `{invG Σ, lftG Σ}.
 Implicit Types κ : lft.
 
 (** Basic borrows  *)
-Lemma bor_create E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx ⊢ ▷ P ={E}=∗ &{κ} P ∗ ([†κ] ={E}=∗ ▷ P).
-Proof. Admitted.
-Lemma bor_fake E κ P :
-  ↑lftN ⊆ E →
-  lft_ctx ⊢ [†κ] ={E}=∗ &{κ}P.
-Proof.
-Admitted.
 Lemma bor_sep E κ P Q :
   ↑lftN ⊆ E →
   lft_ctx ⊢ &{κ} (P ∗ Q) ={E}=∗ &{κ} P ∗ &{κ} Q.
diff --git a/theories/tl_borrow.v b/theories/tl_borrow.v
index b85f4058125674ef1c1f310483c8cc9bfab62953..6cfa358b330c64c7c491a038ba20b09f7a5cfd39 100644
--- a/theories/tl_borrow.v
+++ b/theories/tl_borrow.v
@@ -6,21 +6,21 @@ Definition tl_borrow `{invG Σ, lifetimeG Σ, thread_localG Σ}
            (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
   (∃ i, idx_borrow κ i P ∗ tl_inv tid N (idx_borrow_own 1 i))%I.
 
-Notation "&tl{ κ | tid | N } P" := (tl_borrow κ tid N P)
-  (format "&tl{ κ | tid | N } P", at level 20, right associativity) : uPred_scope.
+Notation "&tl{ κ , tid , N } P" := (tl_borrow κ tid N P)
+  (format "&tl{ κ , tid , N } P", at level 20, right associativity) : uPred_scope.
 
 Section tl_borrow.
   Context `{invG Σ, lifetimeG Σ, thread_localG Σ}
           (tid : thread_id) (N : namespace) (P : iProp Σ).
 
-  Global Instance tl_borrow_persistent κ : PersistentP (&tl{κ|tid|N} P) := _.
+  Global Instance tl_borrow_persistent κ : PersistentP (&tl{κ,tid,N} P) := _.
   Global Instance tl_borrow_proper κ :
     Proper ((⊣⊢) ==> (⊣⊢)) (tl_borrow κ tid N).
   Proof.
     intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
   Qed.
 
-  Lemma borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P.
+  Lemma borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ,tid,N}P.
   Proof.
     iIntros "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]".
     iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
@@ -28,7 +28,7 @@ Section tl_borrow.
 
   Lemma tl_borrow_acc q κ E F :
     nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F →
-    lft_ctx ⊢ &tl{κ|tid|N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
+    lft_ctx ⊢ &tl{κ,tid,N}P -∗ q.[κ] -∗ tl_own tid F ={E}=∗
             ▷P ∗ tl_own tid (F ∖ N) ∗
             (▷P -∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F).
   Proof.
@@ -40,7 +40,7 @@ Section tl_borrow.
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
-  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
+  Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ',tid,N}P -∗ &tl{κ,tid,N}P.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
     iApply (idx_borrow_shorten with "Hκκ' H").