diff --git a/theories/lifetime/accessors.v b/theories/lifetime/accessors.v
index ae90412a50e220dced388e224f6e6b46a4d5ec25..14b6725202b24c055ec6f1f3cd2dc4079e5280a1 100644
--- a/theories/lifetime/accessors.v
+++ b/theories/lifetime/accessors.v
@@ -272,14 +272,40 @@ Proof.
       iApply fupd_intro_mask'. solve_ndisj.
 Qed.
 
+Lemma bor_acc_cons E q κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
+    ∀ Q, ▷ Q -∗ ▷(▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
+Proof.
+  iIntros (?) "#LFT HP Htok".
+  iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
+  iIntros "!>*HQ HPQ". iMod ("Hclose" with "*HQ [HPQ]") as "[Hb $]".
+  - iNext. iIntros "? _". by iApply "HPQ".
+  - iApply (bor_shorten with "Hκκ' Hb").
+Qed.
+
+Lemma bor_acc_atomic_cons E κ P :
+  ↑lftN ⊆ E →
+  lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
+    (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={⊤∖↑lftN}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+    ([†κ] ∗ |={E∖↑lftN,E}=> True).
+Proof.
+  iIntros (?) "#LFT HP".
+  iMod (bor_acc_atomic_strong with "LFT HP") as "[H|[??]]"; first done.
+  - iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>*HQ HPQ".
+    iMod ("Hclose" with "* HQ [HPQ]") as "Hb".
+    + iNext. iIntros "? _". by iApply "HPQ".
+    + iApply (bor_shorten with "Hκκ' Hb").
+  - iRight. by iFrame.
+Qed.
+
 Lemma bor_acc E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ}P -∗ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
 Proof.
   iIntros (?) "#LFT HP Htok".
-  iMod (bor_acc_strong with "LFT HP Htok") as (κ') "(#Hκκ' & $ & Hclose)"; first done.
-  iIntros "!>HP". iMod ("Hclose" with "*HP []") as "[Hb $]". by iIntros "!> $ _".
-  iApply (bor_shorten with "Hκκ' Hb").
+  iMod (bor_acc_cons with "LFT HP Htok") as "($ & Hclose)"; first done.
+  iIntros "!>HP". iMod ("Hclose" with "*HP []") as "[$ $]"; auto.
 Qed.
 
 Lemma bor_acc_atomic E κ P :
@@ -288,9 +314,8 @@ Lemma bor_acc_atomic E κ P :
        (▷ P ∗ (▷ P ={E∖↑lftN,E}=∗ &{κ}P)) ∨ ([†κ] ∗ |={E∖↑lftN,E}=> True).
 Proof.
   iIntros (?) "#LFT HP".
-  iMod (bor_acc_atomic_strong with "LFT HP") as "[H|[H† Hclose]]". done.
-  - iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>HP".
-    iApply (bor_shorten with "Hκκ'"). iApply ("Hclose" with "* HP []"). auto.
+  iMod (bor_acc_atomic_cons with "LFT HP") as "[[HP Hclose]|[? ?]]"; first done.
+  - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "* HP []"); auto.
   - iRight. by iFrame.
 Qed.
 End accessors.
\ No newline at end of file
diff --git a/theories/lifetime/derived.v b/theories/lifetime/derived.v
index 65e6bf460f93d9ae8e49134b633dbd776bd87818..28390da36d5397dfa9c4209ac1e2a4a9986e3b0e 100644
--- a/theories/lifetime/derived.v
+++ b/theories/lifetime/derived.v
@@ -13,10 +13,9 @@ Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
   lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
 Proof.
   iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic_strong with "LFT Hb") as "[H|[H† >_]]"; first done.
-  - iDestruct "H" as (κ') "(Hκκ' & HΦ & Hclose)".
-    iDestruct "HΦ" as (x) "HΦ". iExists x. iApply (bor_shorten with "Hκκ'").
-    iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
+  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
+  - iDestruct "H" as "[HΦ Hclose]". iDestruct "HΦ" as (x) "HΦ".
+    iExists x. iApply ("Hclose" with "HΦ"). iIntros "!> ?"; eauto.
   - iExists inhabitant. by iApply (bor_fake with "LFT").
 Qed.
 
@@ -33,10 +32,9 @@ Lemma bor_later E κ P :
   lft_ctx -∗ &{κ}(▷ P) ={E,E∖↑lftN}▷=∗ &{κ}P.
 Proof.
   iIntros (?) "#LFT Hb".
-  iMod (bor_acc_atomic_strong with "LFT Hb") as "[H|[H† Hclose]]"; first done.
-  - iDestruct "H" as (κ') "(Hκκ' & HP & Hclose)". iModIntro. iNext.
-    iApply (bor_shorten with "Hκκ'"). iApply ("Hclose" with "* HP").
-    by iIntros "!> $ _".
+  iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† Hclose]]"; first done.
+  - iDestruct "H" as "[HP  Hclose]". iModIntro. iNext.
+    iApply ("Hclose" with "* HP"). by iIntros "!> $".
   - iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
 Qed.
 
@@ -45,9 +43,8 @@ Lemma bor_later_tok E q κ P :
   lft_ctx -∗ &{κ}(▷ P) -∗ q.[κ] ={E}▷=∗ &{κ}P ∗ q.[κ].
 Proof.
   iIntros (?) "#LFT Hb Htok".
-  iMod (bor_acc_strong with "LFT Hb Htok") as (κ') "(Hκκ' & HP & Hclose)"; first done.
-  iModIntro. iNext. iMod ("Hclose" with "* HP []") as "[Hb $]". by iIntros "!> $ _".
-  by iApply (bor_shorten with "Hκκ'").
+  iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose]"; first done.
+  iModIntro. iNext. iApply ("Hclose" with "* HP []"). by iIntros "!> $".
 Qed.
 
 Lemma bor_persistent P `{!PersistentP P} E κ q :
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index c390bfcef9d7bd20db71f4268380e4a2ac4a7bcc..b77f8b33887229bda5e7df753feca8702c9fca41 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -51,7 +51,7 @@ Section frac_bor.
       iApply fupd_intro_mask. set_solver. done.
   Qed.
 
-  Lemma frac_bor_acc_strong E q κ Φ:
+  Lemma frac_bor_acc' E q κ Φ:
     ↑lftN ⊆ E →
     lft_ctx -∗ □ (∀ q1 q2, Φ (q1+q2)%Qp ↔ Φ q1 ∗ Φ q2) -∗
     &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
@@ -101,7 +101,7 @@ Section frac_bor.
     ↑lftN ⊆ E →
     lft_ctx -∗ &frac{κ}Φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ Φ q' ∗ (▷ Φ q' ={E}=∗ q.[κ]).
   Proof.
-    iIntros (?) "LFT". iApply (frac_bor_acc_strong with "LFT"). done.
+    iIntros (?) "LFT". iApply (frac_bor_acc' with "LFT"). done.
     iIntros "!#*". rewrite fractional. iSplit; auto.
   Qed.
 
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index 0fc72fa3cb56f922b9dcf814f3d7f2175cc3989b..4cf5f3a0166181a2ce7f1954a980cde7c651e98f 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -273,16 +273,15 @@ Section typing.
     iApply (has_type_wp with "H◁"). iIntros (v) "Hνv H◁!>". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "[Heq H↦]". iDestruct "Heq" as %[=->].
     iMod (lft_incl_acc with "H⊑ Htok") as (q'') "[Htok Hclose]". done.
-    iMod (bor_acc_strong with "LFT H↦ Htok") as (κ0) "(#Hκκ0 & H↦ & Hclose')". done.
+    iMod (bor_acc_cons with "LFT H↦ Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as (l') "(>% & Hown & H†)".
     subst. rewrite heap_mapsto_vec_singleton. wp_read.
     iMod ("Hclose'" with "*[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
     - iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
       iMod (bor_sep with "LFT Hbor") as "[_ Hbor]". done.
-      iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _.
-      iIntros "!>". iSplit. done. iApply (bor_shorten with "Hκκ0 Hbor").
+      iMod ("Hclose" with "Htok") as "$". iFrame "#". iExists _. eauto.
     - iFrame "H↦ H† Hown".
-    - iIntros "!>(?&?&?)_!>". iNext. iExists _.
+    - iIntros "!>(?&?&?)!>". iNext. iExists _.
       rewrite -heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame.
   Qed.