diff --git a/_CoqProject b/_CoqProject
index dbdfbfeb739dded1504322106c0b19b09bca7185..e334a62dafc1d78ef582863c5ba2cec9bfbaef1f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -25,6 +25,7 @@ theories/lang/races.v
 theories/lang/tactics.v
 theories/lang/spawn.v
 theories/typing/type.v
+theories/typing/util.v
 theories/typing/lft_contexts.v
 theories/typing/type_context.v
 theories/typing/cont_context.v
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index a5f90e56a84653914110efa55ed94d6e2da3a961..cfe1fbc3b6576017313a33613843443cb225d01a 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import na_borrow.
-From lrust.typing Require Import typing.
+From lrust.typing Require Import typing util.
 From lrust.typing.lib.refcell Require Import refcell.
 Set Default Proof Using "Type".
 
@@ -56,23 +56,9 @@ Section refmut.
     iDestruct (frac_bor_lft_incl _ _ 1 with "LFT H") as "#Hκν". iClear "H".
     iMod (bor_sep with "LFT Hb") as "[Hb Hαβ]". done.
     iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
-    iExists _, _. iFrame "H↦". rewrite {1}bor_unfold_idx.
-    iDestruct "Hb" as (i) "[#Hpb Hpbown]".
-    iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ⊓ κ) tid lv)%I
-          with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!> !# * % Htok". clear HE.
-    iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
-    iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_unnest with "LFT [Hbtok]") as "Hb". solve_ndisj.
-      { iApply bor_unfold_idx. eauto. }
-      iModIntro. iNext. iMod "Hb".
-      iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
-      { iApply bor_shorten; last done. rewrite -assoc.
-        iApply lft_intersect_mono; first by iApply lft_incl_refl.
-        iApply lft_incl_glb; first done. iApply lft_incl_refl. }
-      iMod ("Hclose" with "[]") as "_"; auto.
-    - iMod ("Hclose" with "[]") as "_". by eauto.
-      iApply step_fupd_intro. set_solver. auto.
+    iExists _, _. iFrame "H↦". iApply delay_sharing_nested; try done.
+    rewrite -assoc. iApply lft_intersect_mono; first by iApply lft_incl_refl.
+    iApply lft_incl_glb; first done. iApply lft_incl_refl.
   Qed.
   Next Obligation.
     iIntros (??????) "#? H". iDestruct "H" as (lv lrc) "[#Hf #H]".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index e8a02e85f33cb48edcbb81eed0bc2940d33fc538..ca13f922e59c1437c7ba83a0107e2f9aee1b82b1 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import na_borrow.
-From lrust.typing Require Import typing.
+From lrust.typing Require Import util typing.
 From lrust.typing.lib.rwlock Require Import rwlock.
 Set Default Proof Using "Type".
 
@@ -44,22 +44,10 @@ Section rwlockwriteguard.
     iMod (bor_sep with "LFT Hb") as "[Hb H]". done.
     iMod (bor_sep with "LFT H") as "[Hαβ _]". done.
     iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
-    iExists _. iFrame "H↦". rewrite {1}bor_unfold_idx.
-    iDestruct "Hb" as (i) "[#Hpb Hpbown]".
-    iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ⊓ κ) tid (shift_loc l' 1))%I
-          with "[Hpbown]") as "#Hinv"; first by eauto.
-    iIntros "!> !# * % Htok". clear HE.
-    iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
-    iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_unnest with "LFT [Hbtok]") as "Hb". solve_ndisj.
-      { iApply bor_unfold_idx. eauto. }
-      iModIntro. iNext. iMod "Hb".
-      iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
-      { iApply (bor_shorten with "[] Hb"). iApply lft_intersect_mono. done.
-        iApply lft_incl_refl. }
-      iMod ("Hclose" with "[]") as "_"; auto.
-    - iMod ("Hclose" with "[]") as "_". by eauto.
-      iApply step_fupd_intro. set_solver. auto.
+    iExists _. iFrame "H↦". iApply delay_sharing_nested; try done.
+    (* FIXME: "iApply lft_intersect_mono" only preserves the later on the last
+       goal, as does "iApply (lft_intersect_mono with ">")". *)
+    iNext. iApply lft_intersect_mono. done. iApply lft_incl_refl.
   Qed.
   Next Obligation.
     iIntros (??????) "#? H". iDestruct "H" as (l') "[#Hf #H]".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 714a149e4234eb7a1e4a8c6b456c1378775fc615..91060a0badd421d9620af802569bb21d401c6c73 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -4,7 +4,7 @@ From iris.base_logic Require Import big_op.
 From lrust.lang Require Export new_delete.
 From lrust.lang Require Import memcpy.
 From lrust.typing Require Export type.
-From lrust.typing Require Import uninit type_context programs.
+From lrust.typing Require Import util uninit type_context programs.
 Set Default Proof Using "Type".
 
 Section own.
@@ -72,18 +72,7 @@ Section own.
     iFrame. iExists l'. rewrite heap_mapsto_vec_singleton.
     iMod (bor_sep with "LFT Hb2") as "[Hb2 _]". set_solver.
     iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
-    rewrite bor_unfold_idx. iDestruct "Hb2" as (i) "(#Hpb&Hpbown)".
-    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]". set_solver.
-    iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_later with "LFT [Hbtok]") as "Hb"; first solve_ndisj.
-      { rewrite bor_unfold_idx. eauto. }
-      iModIntro. iNext. iMod "Hb".
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; first solve_ndisj.
-      iApply "Hclose". auto.
-    - iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
-      iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
+    iApply delay_sharing_later; done.
   Qed.
   Next Obligation.
     intros _ ty κ κ' tid l. iIntros "#Hκ #H".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 401a207842d2b5a2bf7ba065543d13150e4426e6..d39e3a47fcfa487d0cb4c902618a0d43bc44c357 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import big_op.
 From lrust.lang Require Import heap.
 From lrust.typing Require Export type.
-From lrust.typing Require Import lft_contexts type_context shr_bor programs.
+From lrust.typing Require Import util lft_contexts type_context shr_bor programs.
 Set Default Proof Using "Type".
 
 Section uniq_bor.
@@ -28,18 +28,7 @@ Section uniq_bor.
       try (iMod (bor_persistent_tok with "LFT Hb2 Htok") as "[>[] _]"; set_solver).
     iFrame. iExists l'. subst. rewrite heap_mapsto_vec_singleton.
     iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
-    rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
-    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]". set_solver.
-    iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iMod (bor_unnest with "LFT [Hbtok]") as "Hb". solve_ndisj.
-      { iApply bor_unfold_idx. eauto. }
-      iModIntro. iNext. iMod "Hb".
-      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#Hshr $]". solve_ndisj.
-      iMod ("Hclose" with "[]") as "_"; auto.
-    - iMod ("Hclose" with "[]") as "_". by eauto.
-      iApply step_fupd_intro. set_solver. auto.
+    iApply delay_sharing_nested; try done. iApply lft_incl_refl.
   Qed.
   Next Obligation.
     intros κ0 ty κ κ' tid l. iIntros "#Hκ #H".
diff --git a/theories/typing/util.v b/theories/typing/util.v
new file mode 100644
index 0000000000000000000000000000000000000000..68080ca4251aa69988cdd9e349c3a9c9999f1ec0
--- /dev/null
+++ b/theories/typing/util.v
@@ -0,0 +1,58 @@
+From Coq Require Import Qcanon.
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Export type.
+Set Default Proof Using "Type".
+
+Section util.
+  Context `{!typeG Σ}.
+
+  (* Delayed sharing is used by various types; in particular own and uniq.
+     It comes in two flavors: Borrows of "later something" and borrows of
+     "borrowed something".
+     TODO: Figure out a nice way to generalize that; the two proofs below are too
+     similar. *)
+
+
+  Lemma delay_sharing_later N κ l ty tid :
+    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).[κ].
+  Proof.
+    iIntros (?) "#LFT 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
+          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]".
+    - iMod (bor_later with "LFT [Hbtok]") as "Hb"; first solve_ndisj.
+      { rewrite bor_unfold_idx. eauto. }
+      iModIntro. iNext. iMod "Hb".
+      iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; first solve_ndisj.
+      iApply "Hclose". auto.
+    - iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
+      iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
+  Qed.
+
+  Lemma delay_sharing_nested N κ κ' κ'' l ty tid :
+    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).[κ''].
+  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
+          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]".
+    - iMod (bor_unnest with "LFT [Hbtok]") as "Hb". solve_ndisj.
+      { iApply bor_unfold_idx. eauto. }
+      iModIntro. iNext. iMod "Hb".
+      iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
+      { iApply bor_shorten; done. }
+      iMod ("Hclose" with "[]") as "_"; auto.
+    - iMod fupd_intro_mask' as "Hclose'"; last iModIntro. set_solver.
+      iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
+  Qed.
+End util.