diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 5542be3bb928c8674a3cc9b62ec13b13f104f6e3..a2792c74498a5968f9a9d8801eea333fe18777b9 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -43,12 +43,12 @@ Section frac_bor.
     iIntros (?) "#LFT Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done.
     iMod (bor_acc_atomic_strong with "LFT Hφ") as "[H|[H† Hclose]]". done.
     - iDestruct "H" as (κ') "(#Hκκ' & Hφ & Hclose)".
-      iMod ("Hclose" with "[-] []") as "Hφ"; last first.
+      iMod ("Hclose" with "[] [-]") as "Hφ"; last first.
       { iExists γ, κ'. iFrame "#". iApply (bor_share_lftN with "Hφ"); auto. }
-      { iIntros "!>Hφ H†!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
-        iDestruct "Hκ" as (q'') "[_ Hκ]".
-        iDestruct (lft_tok_dead with "Hκ H†") as "[]". }
-      iExists 1%Qp. iFrame. eauto.
+      { iExists 1%Qp. iFrame. eauto. }
+      iIntros "!>Hφ H†!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst.
+      iDestruct "Hκ" as (q'') "[_ Hκ]".
+      iDestruct (lft_tok_dead with "Hκ H†") as "[]".
     - iMod "Hclose" as "_"; last first.
       iExists γ, κ. iSplitR. by iApply lft_incl_refl.
       by iApply shr_bor_fake_lftN.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index ad2291ec71a07fab97cc627319badd15eb7afc68..8feb89a6cc3325df7688c904bbb90d0274b2abe1 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -26,11 +26,11 @@ Implicit Types κ : lft.
 Lemma bor_acc_cons E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ▷ P ∗
-    ∀ Q, ▷ Q -∗ ▷(▷ Q ={∅}=∗ ▷ P) ={E}=∗ &{κ} Q ∗ q.[κ].
+    ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={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 $]".
+  iIntros "!>* HPQ HQ". iMod ("Hclose" with "[HPQ] HQ") as "[Hb $]".
   - iNext. iIntros "? _". by iApply "HPQ".
   - iApply (bor_shorten with "Hκκ' Hb").
 Qed.
@@ -41,7 +41,7 @@ Lemma bor_acc E q κ P :
 Proof.
   iIntros (?) "#LFT HP Htok".
   iMod (bor_acc_cons with "LFT HP Htok") as "($ & Hclose)"; first done.
-  iIntros "!>HP". iMod ("Hclose" with "HP []") as "[$ $]"; auto.
+  iIntros "!>HP". iMod ("Hclose" with "[] HP") as "[$ $]"; auto.
 Qed.
 
 Lemma bor_or E κ P Q :
@@ -59,7 +59,7 @@ Proof.
   iIntros (?) "#LFT Hb".
   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 "!> $".
+    iApply ("Hclose" with "[] HP"). by iIntros "!> $".
   - iIntros "!> !>". iMod "Hclose" as "_". by iApply (bor_fake with "LFT").
 Qed.
 
@@ -83,7 +83,7 @@ Lemma bor_later_tok E q κ P :
 Proof.
   iIntros (?) "#LFT Hb Htok".
   iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose]"; first done.
-  iModIntro. iNext. iApply ("Hclose" with "HP []"). by iIntros "!> $".
+  iModIntro. iNext. iApply ("Hclose" with "[] HP"). by iIntros "!> $".
 Qed.
 
 Lemma bor_persistent P `{!PersistentP P} E κ :
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 5245d4e8f77b8af2eb545a07592c496507029a3a..446e1598c5aea6739ca78feacb4ccc063f523353 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -128,11 +128,11 @@ Module Type lifetime_sig.
                 ([†κ] ∗ |={E∖↑lftN,E}=> idx_bor_own q i).
   Parameter bor_acc_strong : ∀ E q κ P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-      ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
+      ∀ Q, ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].
   Parameter bor_acc_atomic_strong : ∀ E κ P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
       (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-         ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+         ∀ Q, ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
            ([†κ] ∗ |={E∖↑lftN,E}=> True).
 
   (* Because Coq's module system is horrible, we have to repeat properties of lft_incl here
@@ -158,7 +158,7 @@ Module Type lifetime_sig.
     ↑lftN ⊆ E → lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
   Parameter bor_acc_atomic_cons : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-      (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={∅}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+      (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ} Q) ∨
       ([†κ] ∗ |={E∖↑lftN,E}=> True).
   Parameter bor_acc_atomic : ∀ E κ P,
     ↑lftN ⊆ E → lft_ctx -∗ &{κ}P ={E,E∖↑lftN}=∗
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 95012c54969fe8ee7486fc23755347be1a9a1bde..da53e273286c1824b0ff4ee9a8fa19d9c7b86387 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -152,7 +152,7 @@ Qed.
 Lemma bor_acc_strong E q κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P -∗ q.[κ] ={E}=∗ ∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-    ∀ Q, ▷ Q -∗ ▷(▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) ={E}=∗ &{κ'} Q ∗ q.[κ].
+    ∀ Q, ▷(▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E}=∗ &{κ'} Q ∗ q.[κ].
 Proof.
   unfold bor, raw_bor. iIntros (HE) "#LFT Hbor Htok".
   iDestruct "Hbor" as (κ'') "(#Hle & Htmp)". iDestruct "Htmp" as (s'') "(Hbor & #Hs)".
@@ -170,7 +170,7 @@ Proof.
     iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
     { iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
       iLeft. iFrame "%". iExists _, _. iFrame. }
-    iExists κ''. iFrame "#". iIntros "!>*HQ HvsQ". clear -HE.
+    iExists κ''. iFrame "#". iIntros "!>* HvsQ HQ". 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 //
@@ -219,7 +219,7 @@ Lemma bor_acc_atomic_strong E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
    (∃ κ', κ ⊑ κ' ∗ ▷ P ∗
-      ∀ Q, ▷ Q -∗ ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
+      ∀ Q, ▷ (▷ Q -∗ [†κ'] ={∅}=∗ ▷ P) -∗ ▷ Q ={E∖↑lftN,E}=∗ &{κ'} Q) ∨
     ([†κ] ∗ |={E∖↑lftN,E}=> True).
 Proof.
   iIntros (HE) "#LFT Hbor". rewrite bor_unfold_idx /idx_bor /bor /raw_bor.
@@ -238,7 +238,7 @@ Proof.
       as %[EQB%to_borUR_included _]%auth_valid_discrete_2.
     iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
       solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
-    iMod fupd_intro_mask' as "Hclose"; last iIntros "!>*HQ HvsQ". solve_ndisj.
+    iMod fupd_intro_mask' as "Hclose"; last iIntros "!>* HvsQ HQ". solve_ndisj.
     iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
     { iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
     iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
@@ -270,13 +270,13 @@ Qed.
 Lemma bor_acc_atomic_cons E κ P :
   ↑lftN ⊆ E →
   lft_ctx -∗ &{κ} P ={E,E∖↑lftN}=∗
-    (▷ P ∗ ∀ Q, ▷ Q -∗ ▷ (▷ Q ={∅}=∗ ▷ P) ={E∖↑lftN,E}=∗ &{κ} Q) ∨
+    (▷ P ∗ ∀ Q, ▷ (▷ Q ={∅}=∗ ▷ P) -∗ ▷ Q ={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".
+  - iLeft. iDestruct "H" as (κ') "(#Hκκ' & $ & Hclose)". iIntros "!>* HPQ HQ".
+    iMod ("Hclose" with "[HPQ] HQ") as "Hb".
     + iNext. iIntros "? _". by iApply "HPQ".
     + iApply (bor_shorten with "Hκκ' Hb").
   - iRight. by iFrame.
@@ -289,7 +289,7 @@ Lemma bor_acc_atomic E κ P :
 Proof.
   iIntros (?) "#LFT HP".
   iMod (bor_acc_atomic_cons with "LFT HP") as "[[HP Hclose]|[? ?]]"; first done.
-  - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "HP []"); auto.
+  - iLeft. iIntros "!> {$HP} HP". iMod ("Hclose" with "[] HP"); auto.
   - iRight. by iFrame.
 Qed.
 End accessors.
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 22c8f50333fcb4bcdd755f66156bfa308227c36f..5b17cf61b42aa0ce31d5d6a551c2221494f101c8 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -18,7 +18,7 @@ Proof.
   iIntros (?) "#LFT Hb".
   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 x. iApply ("Hclose" with "[] HΦ"). iIntros "!> ?"; eauto.
   - iExists inhabitant. by iApply (bor_fake with "LFT").
 Qed.
 
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 65b4e4fcce33b9742805dd504c2f3a2831fa36fd..4bc0cada0183315cbdba5051eab0d7599291bdb0 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -55,14 +55,14 @@ Section borrow.
     iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
       iDestruct "Hown" as "[Hown H†]". rewrite heap_mapsto_vec_singleton -wp_fupd. wp_read.
     iMod ("Hclose'" $! (l↦#l' ∗ freeable_sz n (ty_size ty) l' ∗ _)%I
-          with "[H↦ Hown H†][]") as "[Hbor Htok]"; last 1 first.
+          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 "($ & $)".
       by rewrite tctx_interp_singleton tctx_hasty_val' //=.
-    - iFrame.
     - iIntros "!>(?&?&?)!>". iNext. iExists _.
       rewrite -heap_mapsto_vec_singleton. iFrame. by iFrame.
+    - iFrame.
   Qed.
 
   Lemma type_deref_uniq_own {E L} κ x p e n ty C T T' :
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index dd1dc515c7e67bd630909a6fe24c4c879a7cfc57..1066f66d7f926084582104ea9a49e7ccd72666ae 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -22,22 +22,33 @@ Definition rc_shrN := rcN .@ "shr".
 Section rc.
   Context `{!typeG Σ, !rcG Σ}.
 
-  Definition rc_inv tid (γ : gname) (l : loc) (ν : lft) (ty : type) : iProp Σ :=
-    (own γ (● None) ∨
-     ∃ q q' c, l ↦ #(Zpos c) ∗ own γ (● Some (q, c)) ∗ †{1%Qp}l…(S ty.(ty_size)) ∗
-            ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗ ty.(ty_shr) ν tid (shift_loc l 1))%I.
+  Definition rc_inv tid ν (γ : gname) (l : loc) (ty : type) : iProp Σ :=
+    (∃ st, own γ (● st) ∗
+      match st with
+      | Some (q, c) => ∃ q',
+       l ↦ #(Zpos c) ∗ †{1%Qp}l…(S ty.(ty_size)) ∗
+         ⌜(q + q')%Qp = 1%Qp⌝ ∗ q'.[ν] ∗
+         (1.[ν] ={↑lftN,∅}▷=∗ ▷ shift_loc l 1 ↦∗: ty.(ty_own) tid)
+      | None => True
+      end)%I.
 
   Program Definition rc (ty : type) :=
     {| ty_size := 1;
        ty_own tid vl :=
          match vl return _ with
-         | [ #(LitLoc l) ] => ∃ γ ν q,
-           na_inv tid rc_invN (rc_inv tid γ l ν ty) ∗ own γ (◯ Some (q, 1%positive)) ∗ q.[ν]
+         | [ #(LitLoc l) ] =>
+           (l ↦ #1 ∗ †{1%Qp}l…(S ty.(ty_size)) ∗ ▷ shift_loc l 1 ↦∗: ty.(ty_own) tid) ∨
+           (∃ γ ν q, na_inv tid rc_invN (rc_inv tid ν γ l ty) ∗
+                     own γ (◯ Some (q, 1%positive)) ∗ q.[ν] ∗
+                     ty.(ty_shr) ν tid (shift_loc l 1))
          | _ => False end;
        ty_shr κ tid l :=
-         ∃ γ ν q (l' : loc), κ ⊑ ν ∗ &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
-                     ▷ na_inv tid rc_invN (rc_inv tid γ l' ν ty) ∗
-                     &na{κ, tid, rc_invN}(own γ (◯ Some (q, 1%positive)))
+         ∃ (l' : loc), &frac{κ} (λ q, l↦∗{q} [ #l']) ∗
+           □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ q.[κ]
+             ={F, F∖↑shrN∖↑lftN}▷=∗ q.[κ] ∗ ∃ γ ν q',
+                na_inv tid rc_invN (rc_inv tid ν γ l' ty) ∗
+                &na{κ, tid, rc_invN}(own γ (◯ Some (q', 1%positive))) ∗
+                ty.(ty_shr) κ tid (shift_loc l' 1)
     |}%I.
   Next Obligation. by iIntros (ty tid [|[[]|][]]) "H". Qed.
   Next Obligation.
@@ -47,23 +58,64 @@ Section rc.
     iMod (bor_fracture (λ q, l ↦∗{q} vl)%I with "LFT H↦") as "#H↦"; first done.
     destruct vl as [|[[|l'|]|][|]];
       try by iMod (bor_persistent_tok with "LFT Hb Htok") as "[>[] _]".
-    iMod (bor_exists with "LFT Hb") as (γ) "Hb"; first done.
-    iMod (bor_exists with "LFT Hb") as (ν) "Hb"; first done.
-    iMod (bor_exists with "LFT Hb") as (q') "Hb"; first done.
-    iMod (bor_sep with "LFT Hb") as "[Hinv Hb]"; first done.
-    iMod (bor_persistent_tok with "LFT Hinv Htok") as "[#Hinv Htok]"; first done.
-    iMod (bor_sep with "LFT Hb") as "[Hrc Hlft]"; first done.
-    iDestruct (frac_bor_lft_incl with "LFT >[Hlft]") as "#Hlft".
-    { iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
-    iMod (bor_na with "Hrc") as "#Hrc"; first done.
-    eauto 20.
+    iFrame "Htok". iExists _. iFrame "#". rewrite bor_unfold_idx.
+    iDestruct "Hb" as (i) "(#Hpb&Hpbown)".
+    set (C := (∃ _ _ _, _ ∗ &na{_,_,_} _ ∗ _)%I).
+    iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ C)%I
+          with "[Hpbown]") as "#Hinv"; first by iLeft.
+    iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first set_solver.
+    iDestruct "INV" as "[>Hbtok|#Hshr]".
+    - iAssert (&{κ} _)%I with "[Hbtok]" as "Hb".
+      { rewrite bor_unfold_idx. iExists _. by iFrame. }
+      iClear "H↦ Hinv Hpb".
+      iMod (bor_acc_cons with "LFT Hb Htok") as "[HP Hclose2]"; first solve_ndisj.
+      set (X := (∃ _ _ _, _)%I).
+      (* TODO: Would be nice to have a lemma for the next two lines. *)
+      iMod fupd_intro_mask' as "Hclose3"; last iModIntro; first solve_ndisj. iNext.
+      iMod "Hclose3" as "_". iAssert (|={F ∖ ↑shrN}=> X )%I with "[HP]" as ">HX".
+      { iDestruct "HP" as "[[Hl' [H† Hown]]|$]"; last done.
+        iMod (lft_create with "LFT") as (ν) "[[Hν1 Hν2] #Hν†]"; first solve_ndisj.
+        (* TODO: We should consider changing the statement of bor_create to dis-entangle the two masks such that this is no longer necessary. *)
+        iApply (fupd_mask_mono (↑lftN)); first solve_ndisj.
+        iMod (bor_create with "LFT Hown") as "[HP HPend]"; first solve_ndisj.
+        iMod (own_alloc (● Some ((1/2)%Qp, 1%positive) ⋅ ◯ Some ((1/2)%Qp, 1%positive))) as (γ) "[Ha Hf]".
+        { apply auth_valid_discrete_2. done. }
+        iMod (na_inv_alloc tid _ _ (rc_inv tid ν γ l' ty) with "[Ha Hν2 Hl' H† HPend]").
+        { rewrite /rc_inv. iExists (Some (_, _)). iFrame. iExists _. iFrame.
+          iNext. iSplit; first by rewrite Qp_div_2. iIntros "Hν".
+          iMod ("Hν†" with "Hν") as "Hfin". iModIntro. iNext. iMod "Hfin".
+          iMod ("HPend" with "Hfin"). done. }
+        iMod (ty_share with "LFT HP Hν1") as "[??]"; first solve_ndisj.
+        iExists _, _, _. iFrame. done. }
+      iDestruct "HX" as (γ ν q') "(#Hinv & Hrc & Htok & #Hshr)".
+      iMod ("Hclose2" with "[] [Hrc Htok]") as "[HX Htok]".
+      { iNext. iIntros "HX". iModIntro. (* FIXME: iNext here doesn't strip of the next from in front of the evar. *)
+        iRight. iExists γ, ν, q'. iExact "HX". }
+      { iNext. by iFrame "#∗". }
+      iAssert (|={F ∖ ↑shrN}=> C)%I with "[HX]" as ">#HC".
+      { iExists _, _, _. iFrame "Hinv".
+        iMod (bor_sep with "LFT HX") as "[_ HX]"; first solve_ndisj.
+        iMod (bor_sep with "LFT HX") as "[Hrc HX]"; first solve_ndisj.
+        iMod (bor_sep with "LFT HX") as "[Hlft _]"; first solve_ndisj.
+        iDestruct (frac_bor_lft_incl with "LFT >[Hlft]") as "#Hlft".
+        { iApply (bor_fracture with "LFT"); first solve_ndisj. by rewrite Qp_mult_1_r. }
+        iMod (bor_na with "Hrc") as "$"; first solve_ndisj.
+        iApply ty_shr_mono; done. }
+      iMod ("Hclose" with "[]") as "_"; first by auto.
+      by iFrame "#∗".
+    - iMod ("Hclose" with "[]") as "_"; first by auto.
+      iApply step_fupd_intro; first solve_ndisj. iNext. by iFrame.
   Qed.
   Next Obligation.
-    iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (????) "#H".
-    do 4 iExists _. iDestruct "H" as "(? & ? & $ & ?)".
-    iSplit; last iSplit.
-    - by iApply lft_incl_trans.
-    - by iApply frac_bor_shorten.
+    iIntros (ty κ κ' tid l) "#Hincl H". iDestruct "H" as (l') "[#Hl #Hshr]".
+    iExists _. iSplit; first by iApply frac_bor_shorten.
+    iAlways. iIntros (F q) "% Htok".
+    iMod (lft_incl_acc with "Hincl Htok") as (q'') "[Htok Hclose]"; first solve_ndisj.
+    iMod ("Hshr" with "[] Htok") as "Hshr2"; first done.
+    iModIntro. iNext. iMod "Hshr2" as "[Htok HX]".
+    iMod ("Hclose" with "Htok") as "$". iDestruct "HX" as (???) "(? & ? & ?)".
+    iExists _, _, _. iModIntro. iFrame. iSplit.
     - by iApply na_bor_shorten.
+    - by iApply ty_shr_mono.
   Qed.
 End rc.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 9523a646d1cc8b399bc36c815a3313c4b5f68848..ac4a31ed9431bb3394513286d7ba7cb02bcdfd8b 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -115,17 +115,17 @@ Section refcell.
     iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
     iDestruct "H" as "[>% Hown]".
     iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ n⌝) ∗
-            shift_loc l 1 ↦∗: ty.(ty_own) tid) with "[-] []")%I as "[H [Htok Htok']]".
-    { iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
-      iSplitL "Hn"; [eauto|iExists _; iFrame]. }
+            shift_loc l 1 ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
     { iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
       iDestruct "Hvl" as (vl') "[H↦ Hvl]".
       iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗%". }
+    { iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
+      iSplitL "Hn"; [eauto|iExists _; iFrame]. }
     iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
     iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
     iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, refcell_inv tid l γ κ ty)%I with ">[-Hclose]"
       as "[$ HQ]"; last first.
-    { iMod ("Hclose" with "HQ []") as "[Hb $]".
+    { iMod ("Hclose" with "[] HQ") as "[Hb $]".
       - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
         iExists _. iIntros "{$H}!%". destruct st as [[?[|[]|]]|]; simpl; lia.
       - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 1c3421925f4b2ba24b85650b32abc6668bdc7e50..f8abf1333c5a1f4c8b984c2e01aefb1c4d2bd57b 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -110,17 +110,17 @@ Section rwlock.
     iDestruct "H" as ([|[[| |n]|]vl]) "[H↦ H]"; try iDestruct "H" as ">[]".
     iDestruct "H" as "[>% Hown]".
     iMod ("Hclose" $! ((∃ n:Z, l ↦ #n ∗ ⌜-1 ≤ n⌝) ∗
-            shift_loc l 1 ↦∗: ty.(ty_own) tid) with "[-] []")%I as "[H [Htok Htok']]".
-    { iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
-      iSplitL "Hn"; [eauto|iExists _; iFrame]. }
+            shift_loc l 1 ↦∗: ty.(ty_own) tid) with "[] [-]")%I as "[H [Htok Htok']]".
     { iIntros "!> [Hn Hvl] !>". iDestruct "Hn" as (n') "[Hn >%]".
       iDestruct "Hvl" as (vl') "[H↦ Hvl]".
       iExists (#n'::vl'). rewrite heap_mapsto_vec_cons. iFrame "∗%". }
+    { iNext. rewrite heap_mapsto_vec_cons. iDestruct "H↦" as "[Hn Hvl]".
+      iSplitL "Hn"; [eauto|iExists _; iFrame]. }
     iMod (bor_sep with "LFT H") as "[Hn Hvl]". done.
     iMod (bor_acc_cons with "LFT Hn Htok") as "[H Hclose]". done.
     iAssert ((q / 2).[κ] ∗ ▷ ∃ γ, rwlock_inv tid l γ κ ty)%I with ">[-Hclose]"
       as "[$ HQ]"; last first.
-    { iMod ("Hclose" with "HQ []") as "[Hb $]".
+    { iMod ("Hclose" with "[] HQ") as "[Hb $]".
       - iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
         iExists _. iIntros "{$H}!%". destruct st as [[|[[]?]|]|]; simpl; lia.
       - iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 7513bbd09822f4f960b6e7abb5c376243eae174a..da864583303e6b2a5051866f3e994023a127b20d 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -77,19 +77,19 @@ Section case.
     iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'.
     destruct Hety as [Hety|Hety].
     - iMod ("Hclose'" $! (shift_loc l 1 ↦∗: ty.(ty_own) tid)%I
-            with "[H↦vl' Hown] [H↦i H↦vl'']") as "[Hb Htok]".
-      { iExists vl'. iFrame. }
+            with "[H↦i H↦vl''] [H↦vl' Hown]") as "[Hb Htok]".
       { iIntros "!>Hown". iDestruct "Hown" as (vl'2) "[H↦ Hown]".
         iExists (#i::vl'2++vl''). iIntros "!>". iNext.
         iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
         rewrite heap_mapsto_vec_cons heap_mapsto_vec_app EQlenvl' EQlenvl'2.
         iFrame. iExists _, _, _. iSplit. by auto.
         rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
+      { iExists vl'. iFrame. }
       iMod ("Hclose" with "Htok") as "[HE HL]".
       iApply (Hety with "LFT Hna HE HL HC").
       rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
-    - iMod ("Hclose'" with "[H↦i H↦vl' H↦vl'' Hown] []") as "[Hb Htok]";
-        [|by iIntros "!>$"|].
+    - iMod ("Hclose'" with "[] [H↦i H↦vl' H↦vl'' Hown]") as "[Hb Htok]";
+        [by iIntros "!>$"| |].
       { iExists (#i::vl'++vl'').
         rewrite heap_mapsto_vec_cons heap_mapsto_vec_app -EQlen. iFrame. iNext.
         iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 68080ca4251aa69988cdd9e349c3a9c9999f1ec0..c67cc8abd949e893bb03e673f7431409f1cd502b 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -12,6 +12,15 @@ Section util.
      TODO: Figure out a nice way to generalize that; the two proofs below are too
      similar. *)
 
+  (* This is somewhat the general pattern here... but it doesn't seem easy to make
+     this usable in Coq, with the arbitrary quantifiers and things.  Also, it actually works
+     not just for borrows but for anything that you can split into a timeless and a persistent part.
+  Lemma delay_borrow_step :
+    lfeE ⊆ N → (∀ x, PersistentP (Post x)) →
+    lft_ctx -∗ &{κ} P -∗
+      □ (∀ x, &{κ} P -∗ Pre x -∗ Frame x ={F1,F2}▷=∗ Post x ∗ Frame x) ={N}=∗ 
+      □ (∀ x, Pre x -∗ Frame x ={F1,F2}▷=∗ Post x ∗ Frame x).
+   *)
 
   Lemma delay_sharing_later N κ l ty tid :
     lftE ⊆ N →
@@ -38,11 +47,11 @@ Section util.
     lftE ⊆ N →
     lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'} &{κ} l ↦∗: ty_own ty tid ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
-       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN ∖ ↑lftN}▷=∗ ty.(ty_shr) (κ'') tid l ∗ (q).[κ''].
+       ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN ∖ ↑lftN}▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
   Proof.
     iIntros (?) "#LFT #Hincl Hbor". rewrite bor_unfold_idx.
     iDestruct "Hbor" as (i) "(#Hpb&Hpbown)".
-    iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (κ'') tid l)%I
+    iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty κ'' tid l)%I
           with "[Hpbown]") as "#Hinv"; first by eauto.
     iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]"; first set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".