diff --git a/theories/typing/lib/slice/slice.v b/theories/typing/lib/slice/slice.v
index c83945abdddfa6dd61c5ef97791a7aee5da51149..3cb66a63aa70364b761749491a916b2c08192dc0 100644
--- a/theories/typing/lib/slice/slice.v
+++ b/theories/typing/lib/slice/slice.v
@@ -7,12 +7,11 @@ Implicit Type 𝔄 𝔅: syn_type.
 Section slice.
   Context `{!typeG Σ}.
 
-  Lemma split_mt_shr_slice {A} φ Φ l' d q :
-    (l' ↦∗{q}: (λ vl, [S(d') := d]
-      ∃(l: loc) (n: nat) (aπl: A n),
-        ⌜vl = [ #l; #n] ∧ φ n aπl⌝ ∗ Φ l n d' aπl)) ⊣⊢
+  Lemma split_mt_shr_slice {A} d φ Φ l' q :
+    (l' ↦∗{q}: (λ vl, [S(d') := d] ∃(l: loc) (n: nat) (aπl: A n),
+      ⌜vl = [ #l; #n] ∧ φ n aπl⌝ ∗ Φ d' l n aπl)) ⊣⊢
     [S(d') := d] ∃(l: loc) (n: nat) (aπl: A n),
-      ⌜φ n aπl⌝ ∗ l' ↦{q} #l ∗ (l' +ₗ 1) ↦{q} #n ∗ Φ l n d' aπl.
+      ⌜φ n aπl⌝ ∗ l' ↦{q} #l ∗ (l' +ₗ 1) ↦{q} #n ∗ Φ d' l n aπl.
   Proof.
     iSplit.
     - iIntros "(%& ↦ & big)". case d; [done|]=>/= ?.
@@ -24,6 +23,16 @@ Section slice.
       iExists _, _, _. by iFrame.
   Qed.
 
+  Lemma split_mt_shr_slice' {A} φ Φ l' q :
+    (l' ↦∗{q}: (λ vl, ∃(l: loc) (n: nat) (aπl: A n),
+      ⌜vl = [ #l; #n] ∧ φ n aπl⌝ ∗ Φ l n aπl)) ⊣⊢
+    ∃(l: loc) (n: nat) (aπl: A n),
+      ⌜φ n aπl⌝ ∗ l' ↦{q} #l ∗ (l' +ₗ 1) ↦{q} #n ∗ Φ l n aπl.
+  Proof.
+    set Φ' := λ _: nat, Φ. have ->: Φ = Φ' 0%nat by done.
+    by apply (split_mt_shr_slice (S _)).
+  Qed.
+
   (* Rust's &'a [T] *)
   Program Definition shr_slice {𝔄} (κ: lft) (ty: type 𝔄) : type (listₛ 𝔄) := {|
     st_size := 2;  st_lfts := κ :: ty.(ty_lfts);  st_E := ty.(ty_E) ++ ty_outlives_E ty κ;
diff --git a/theories/typing/lib/smallvec/smallvec_index.v b/theories/typing/lib/smallvec/smallvec_index.v
index 9c49ecb1749eb78f60a6fbf6d51a1b71a54ab812..02199fc10d3643879b9733d89d1fd44888dc9ad5 100644
--- a/theories/typing/lib/smallvec/smallvec_index.v
+++ b/theories/typing/lib/smallvec/smallvec_index.v
@@ -52,9 +52,9 @@ Section smallvec_index.
       iApply ("C" $! [# #_] -[aπl !!! ifin] with "Na L [-] []").
       + iSplit; [|done]. rewrite tctx_hasty_val. iExists (S (S d)).
         iSplit. { iApply persistent_time_receipt_mono; [|done]. lia. }
-        rewrite/= freeable_sz_full. iFrame "†r". iNext. iExists [_].
-        rewrite heap_mapsto_vec_singleton. iFrame "↦r".
-        rewrite/= -Nat2Z.inj_mul Eqi. iApply (big_sepL_vlookup with "tys").
+        rewrite/= freeable_sz_full. iFrame "†r". iNext. rewrite split_mt_ptr'.
+        iExists _. iFrame "↦r". rewrite/= -Nat2Z.inj_mul Eqi.
+        iApply (big_sepL_vlookup with "tys").
       + iApply proph_obs_impl; [|done]=>/= ?[?[?[/Nat2Z.inj <-[++]]]].
         by rewrite Eqi -vlookup_lookup -vapply_lookup=> <-.
     - wp_read. wp_op. do 2 wp_read. do 2 wp_op. wp_write.
@@ -69,9 +69,9 @@ Section smallvec_index.
       iApply ("C" $! [# #_] -[aπl !!! ifin] with "Na L [-] []").
       + iSplit; [|done]. rewrite tctx_hasty_val. iExists (S (S d)).
         iSplit. { iApply persistent_time_receipt_mono; [|done]. lia. }
-        rewrite/= freeable_sz_full. iFrame "†r". iNext. iExists [_].
-        rewrite heap_mapsto_vec_singleton. iFrame "↦r".
-        rewrite/= -Nat2Z.inj_mul Eqi. iApply (big_sepL_vlookup with "tys").
+        rewrite/= freeable_sz_full. iFrame "†r". iNext. rewrite split_mt_ptr'.
+        iExists _. iFrame "↦r". rewrite/= -Nat2Z.inj_mul Eqi.
+        iApply (big_sepL_vlookup with "tys").
       + iApply proph_obs_impl; [|done]=>/= ?[?[?[/Nat2Z.inj <-[++]]]].
         by rewrite Eqi -vlookup_lookup -vapply_lookup=> <-.
   Qed.
@@ -140,10 +140,9 @@ Section smallvec_index.
       + rewrite cctx_interp_singleton.
         iMod ("ToL" with "[$α $α₊ $α₊₊] L") as "L".
         iApply ("C" $! [# #_] -[λ π, ((aπl !!! ifin) π, π ζ)] with "Na L [-] []").
-        * iSplitL; [|done]. rewrite tctx_hasty_val. iExists _.
-          rewrite -freeable_sz_full. iFrame "⧖ †r". iNext. iExists [_].
-          rewrite heap_mapsto_vec_singleton. iFrame "↦r In". iExists d', _.
-          iFrame "Vo' Bor". iPureIntro. split; [lia|done].
+        * iSplitL; [|done]. rewrite tctx_hasty_val. iExists (S _).
+          rewrite/= -freeable_sz_full split_mt_uniq_bor. iFrame "⧖ †r In". iNext.
+          iExists _, d', _. iFrame "↦r Vo' Bor". iPureIntro. split; [lia|done].
         * iApply proph_obs_impl; [|done]=>/= ?[[?[?[/Nat2Z.inj <-[++]]]]Eqξ].
           rewrite Eqi -vlookup_lookup=> <- Imp. rewrite -vapply_lookup. apply Imp.
           by rewrite Eqξ -vec_to_list_apply vapply_insert -vec_to_list_insert.
diff --git a/theories/typing/lib/vec/vec.v b/theories/typing/lib/vec/vec.v
index a768d99f0954d12d6ecd4dbf54ed9a15291f5642..202da45fdfb839e4b2b8250e8b204d87764a0fa5 100644
--- a/theories/typing/lib/vec/vec.v
+++ b/theories/typing/lib/vec/vec.v
@@ -8,7 +8,7 @@ Implicit Type 𝔄 𝔅: syn_type.
 Section vec.
   Context `{!typeG Σ}.
 
-  Lemma split_mt_vec {𝔄} l' d alπ Φ :
+  Lemma split_mt_vec {𝔄} d l' alπ Φ :
     (l' ↦∗: (λ vl, [S(d') := d] ∃(l: loc) (len ex: nat) (aπl: vec (proph 𝔄) len),
       ⌜vl = [ #l; #len; #ex] ∧ alπ = lapply aπl⌝ ∗ Φ d' l len ex aπl)) ⊣⊢
     [S(d') := d] ∃(l: loc) (len ex: nat) (aπl: vec (proph 𝔄) len),
@@ -21,6 +21,16 @@ Section vec.
       iExists [_;_;_]. iFrame "↦". iExists _, _, _, _. by iFrame.
   Qed.
 
+  Lemma split_mt_vec' {𝔄} l' alπ Φ :
+    (l' ↦∗: (λ vl, ∃(l: loc) (len ex: nat) (aπl: vec (proph 𝔄) len),
+      ⌜vl = [ #l; #len; #ex] ∧ alπ = lapply aπl⌝ ∗ Φ l len ex aπl)) ⊣⊢
+    ∃(l: loc) (len ex: nat) (aπl: vec (proph 𝔄) len),
+      ⌜alπ = lapply aπl⌝ ∗ l' ↦∗ [ #l; #len; #ex] ∗ Φ l len ex aπl.
+  Proof.
+    set Φ' := λ _: nat, Φ. have ->: Φ = Φ' 0 by done.
+    by apply (split_mt_vec (S _)).
+  Qed.
+
   (* Rust's Vec<T> *)
   Program Definition vec_ty {𝔄} (ty: type 𝔄) : type (listₛ 𝔄) := {|
     ty_size := 3;  ty_lfts := ty.(ty_lfts);  ty_E := ty.(ty_E);
diff --git a/theories/typing/lib/vec/vec_basic.v b/theories/typing/lib/vec/vec_basic.v
index b405b63829ea75d54707b3a58cd011916eab0d5a..865c9c4092fd53298b45d1428bc2f6c550d385c3 100644
--- a/theories/typing/lib/vec/vec_basic.v
+++ b/theories/typing/lib/vec/vec_basic.v
@@ -97,11 +97,10 @@ Section vec_basic.
     iIntros "⧖". wp_seq. wp_op. wp_write. wp_op. wp_write. do 2 wp_seq.
     rewrite cctx_interp_singleton.
     iApply ("C" $! [# #_] -[const []] with "Na L [-Obs] Obs"). iSplit; [|done].
-    iExists _, _. do 2 (iSplit; [done|]). rewrite/= freeable_sz_full.
-    iFrame "†". iNext. iExists [_; _; _].
-    rewrite !heap_mapsto_vec_cons shift_loc_assoc heap_mapsto_vec_nil.
-    iFrame "↦₀ ↦₁ ↦₂". iExists l, 0, 0, [#]. iSplit; [done|]. iFrame "†'".
-    iSplit; [by iNext|]. iExists []. by rewrite heap_mapsto_vec_nil.
+    iExists _, _. do 2 (iSplit; [done|]). rewrite/= freeable_sz_full split_mt_vec'.
+    iFrame "†". iNext. iExists _, 0, 0, [#]=>/=. iSplit; [done|].
+    rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil shift_loc_assoc.
+    iFrame "↦₀ ↦₁ ↦₂ †'". iSplit; [by iNext|]. iExists []. by rewrite heap_mapsto_vec_nil.
   Qed.
 
   Definition vec_drop {𝔄} (ty: type 𝔄) : val :=
diff --git a/theories/typing/lib/vec/vec_index.v b/theories/typing/lib/vec/vec_index.v
index e1294ecf950cf39083ad74d9f6a912c25c991faa..8b93a9d6d385f719401c66189cbd4f3499b8fabf 100644
--- a/theories/typing/lib/vec/vec_index.v
+++ b/theories/typing/lib/vec/vec_index.v
@@ -46,9 +46,8 @@ Section vec_index.
     iApply ("C" $! [# #_] -[aπl !!! ifin] with "Na L [-] []").
     - iSplit; [|done]. rewrite tctx_hasty_val. iExists (S (S d)).
       iSplit. { iApply persistent_time_receipt_mono; [|done]. lia. }
-      rewrite/= freeable_sz_full. iFrame "†r". iNext. iExists [_].
-      rewrite heap_mapsto_vec_singleton. iFrame "↦r".
-      rewrite/= -Nat2Z.inj_mul Eqi. iApply (big_sepL_vlookup with "tys").
+      rewrite/= freeable_sz_full split_mt_ptr'. iFrame "†r". iNext. iExists _.
+      iFrame "↦r". rewrite/= -Nat2Z.inj_mul Eqi. iApply (big_sepL_vlookup with "tys").
     - iApply proph_obs_impl; [|done]=>/= ?[?[?[/Nat2Z.inj <-[++]]]].
       by rewrite Eqi -vlookup_lookup -vapply_lookup=> <-.
   Qed.
@@ -117,10 +116,9 @@ Section vec_index.
     - rewrite cctx_interp_singleton.
       iMod ("ToL" with "[$α $α₊ $α₊₊] L") as "L".
       iApply ("C" $! [# #_] -[λ π, ((aπl !!! ifin) π, π ζ)] with "Na L [-] []").
-      + iSplitL; [|done]. rewrite tctx_hasty_val. iExists _.
-        rewrite -freeable_sz_full. iFrame "⧖ †r". iNext. iExists [_].
-        rewrite heap_mapsto_vec_singleton. iFrame "↦r In". iExists d', _.
-        iFrame "Vo' Bor". iPureIntro. split; [lia|done].
+      + iSplitL; [|done]. rewrite tctx_hasty_val. iExists (S _).
+        rewrite/= -freeable_sz_full split_mt_uniq_bor. iFrame "⧖ †r In". iNext.
+        iExists _, d', _. iFrame "↦r Vo' Bor". iPureIntro. split; [lia|done].
       + iApply proph_obs_impl; [|done]=>/= ?[[?[?[/Nat2Z.inj <-[++]]]]Eqξ].
         rewrite Eqi -vlookup_lookup=> <- Imp. rewrite -vapply_lookup. apply Imp.
         by rewrite Eqξ -vec_to_list_apply vapply_insert -vec_to_list_insert.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 16cf5bc58ef7fed6a0e15f2c318752e876069bc6..01e735e5a171d519311988eb69f42f1bbf055da3 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -1169,7 +1169,7 @@ Section type_util.
   Context `{!typeG Σ}.
 
   (* Splitting for a standard pointer *)
-  Lemma split_mt_ptr Φ d l' :
+  Lemma split_mt_ptr d Φ l' :
     (l' ↦∗: λ vl, [S(d') := d] [loc[l] := vl] Φ d' l) ⊣⊢
     [S(d') := d] ∃l: loc, l' ↦ #l ∗ Φ d' l.
   Proof.
@@ -1180,6 +1180,13 @@ Section type_util.
       iExists [_]. rewrite heap_mapsto_vec_singleton. by iFrame.
   Qed.
 
+  Lemma split_mt_ptr' Φ l' :
+    (l' ↦∗: λ vl, [loc[l] := vl] Φ l) ⊣⊢ ∃l: loc, l' ↦ #l ∗ Φ l.
+  Proof.
+    set Φ' := λ _: nat, Φ. have ->: Φ = Φ' 0%nat by done.
+    by apply (split_mt_ptr (S _)).
+  Qed.
+
   Lemma heap_mapsto_ty_own {𝔄} l (ty: type 𝔄) vπ d tid :
     l ↦∗: ty.(ty_own) vπ d tid ⊣⊢
     ∃vl: vec val ty.(ty_size), l ↦∗ vl ∗ ty.(ty_own) vπ d tid vl.