diff --git a/theories/typing/lib/smallvec/smallvec.v b/theories/typing/lib/smallvec/smallvec.v
index 499607aabb635eac1b96a2ca48f63b568d9a7d51..135a923ac5af603e70dbed3e2d3595fe87e65bcd 100644
--- a/theories/typing/lib/smallvec/smallvec.v
+++ b/theories/typing/lib/smallvec/smallvec.v
@@ -47,19 +47,19 @@ Section smallvec.
         ([∗ list] i ↦ aπ ∈ aπl, (l' +ₗ 4 +ₗ[ty] i) ↦∗: ty.(ty_own) aπ d tid) ∗
         ∃wl', ⌜k = (len * ty.(ty_size) + length wl')%nat⌝ ∗ (l' +ₗ 4 +ₗ[ty] len) ↦∗ wl'
       else (* vector mode *)
-        ∃wl, ⌜length wl = k⌝ ∗ (l' +ₗ 4) ↦∗ wl ∗ Φ l len ex aπl.
+        (∃wl, ⌜length wl = k⌝ ∗ (l' +ₗ 4) ↦∗ wl) ∗ Φ l len ex aπl.
   Proof.
     iSplit.
     - iIntros "(%& ↦ & big)". iDestruct "big" as (b ?????(->&?&?)) "big".
       iExists _, _, _, _, _. iSplit; [done|].
       rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
-      iDestruct "↦" as "($&$&$&$& ↦)". case b; [|iExists _; by iFrame].
-      iDestruct "big" as (??->) "tys/=".
+      iDestruct "↦" as "($&$&$&$& ↦)". case b=>/=; last first.
+      { iFrame "big". iExists _. by iFrame. } iDestruct "big" as (??->) "tys/=".
       iDestruct (big_sepL_ty_own_length with "tys") as %<-.
       rewrite heap_mapsto_vec_app trans_big_sepL_mt_ty_own shift_loc_assoc.
       iDestruct "↦" as "[? ↦ex]". iSplitR "↦ex"; iExists _; iFrame.
       by rewrite -app_length.
-    - iDestruct 1 as (b ?????) "(↦hd & big)". case b.
+    - iDestruct 1 as (b ?????) "(↦hd & big)". case b=>/=.
       + rewrite trans_big_sepL_mt_ty_own.
         iDestruct "big" as "[(%wll & ↦ar & tys) (%wl' &->& ↦ex)]".
         iDestruct (big_sepL_ty_own_length with "tys") as %Eqsz.
@@ -68,10 +68,10 @@ Section smallvec.
         iDestruct "↦hd" as "($&$&$&$&_)". iFrame "↦ar ↦ex".
         iExists true, _, _, _, _, _. iSplit; [by rewrite -app_length|].
         iExists _, _. by iFrame.
-      + iDestruct "big" as (?<-) "[↦tl ?]". iExists ([_;_;_;_]++_).
+      + iDestruct "big" as "[(%&%&↦tl) ?]". iExists ([_;_;_;_]++_).
         rewrite !heap_mapsto_vec_cons !shift_loc_assoc.
         iDestruct "↦hd" as "($&$&$&$&_)". iFrame "↦tl".
-        iExists false, _, _, _, _, _. by iFrame.
+        iExists false, _, _, _, _, _=>/=. by iFrame.
   Qed.
 
   (* For simplicity, it always has the location and capacity *)
@@ -123,9 +123,7 @@ Section smallvec.
       iMod (ty_share_big_sepL with "LFT In Bor κ") as "Toshrs"; [done|].
       iApply (step_fupdN_wand with "Toshrs"). iIntros "!> >[?$] !>".
       iExists true, _, _, _, _. by iFrame.
-    - iMod (bor_exists with "LFT Bor") as (?) "Bor"; [done|].
-      iMod (bor_sep_persistent with "LFT Bor κ") as "(_ & Bor & κ)"; [done|].
-      iMod (bor_sep with "LFT Bor") as "[_ Bor]"; [done|].
+    - iMod (bor_sep with "LFT Bor") as "[_ Bor]"; [done|].
       iMod (bor_sep with "LFT Bor") as "[Bor _]"; [done|].
       iMod (ty_share_big_sepL with "LFT In Bor κ") as "Toshrs"; [done|].
       iApply (step_fupdN_wand with "Toshrs"). iIntros "!> >[?$] !>".
@@ -165,5 +163,4 @@ Section smallvec.
 
   Global Instance smallvec_ne {𝔄} n : NonExpansive (@smallvec 𝔄 n).
   Proof. solve_ne_type. Qed.
-
 End smallvec.
diff --git a/theories/typing/lib/smallvec/smallvec_basic.v b/theories/typing/lib/smallvec/smallvec_basic.v
index 68d14d4761dfb749ba57fa7c1f44dbe383bda22b..9515cde6c5c4110471f5c636d1a0db561c2dd0c2 100644
--- a/theories/typing/lib/smallvec/smallvec_basic.v
+++ b/theories/typing/lib/smallvec/smallvec_basic.v
@@ -158,8 +158,8 @@ Section smallvec_basic.
       iApply ("C" $! [# #_] -[const ()] with "Na L [-Obs] Obs"). iSplit; [|done].
       rewrite tctx_hasty_val. iExists _. iFrame "⧖". iSplit; [|done]. iNext.
       iExists _. iFrame "↦". by rewrite unit_ty_own.
-    - iDestruct "big" as (? <-) "big". rewrite trans_big_sepL_mt_ty_own.
-      iDestruct "big" as "(↦tl & (%& ↦ar & tys) & (%& %Eq & ↦ex) & †')".
+    - rewrite trans_big_sepL_mt_ty_own.
+      iDestruct "big" as "((%&<-& ↦tl) & (%& ↦ar & tys) & (%& %Eq & ↦ex) & †')".
       iDestruct (big_sepL_ty_own_length with "tys") as %Eq'.
       do 2 (wp_op; wp_read). do 3 wp_op. wp_read.
       rewrite -Nat2Z.inj_add -Nat2Z.inj_mul !Nat.mul_add_distr_r -Eq -Eq' -app_length.
diff --git a/theories/typing/lib/smallvec/smallvec_index.v b/theories/typing/lib/smallvec/smallvec_index.v
index 9ee580befcf7cb0e7823f1516fd78494c599fa82..fb0d6fb02cbe7c9862897a54a096b334d58de5bc 100644
--- a/theories/typing/lib/smallvec/smallvec_index.v
+++ b/theories/typing/lib/smallvec/smallvec_index.v
@@ -163,7 +163,7 @@ Section smallvec_index.
         setoid_rewrite shift_loc_assoc. iSplitL "↦ty".
         { iStopProof. do 3 f_equiv. iApply ty_own_depth_mono. lia. }
         iStopProof. do 6 f_equiv; [|iApply ty_own_depth_mono; lia]. do 2 f_equiv. lia.
-    - iDestruct "big" as (??) "(↦tl & ↦tys & ex†)". wp_read. wp_op. do 2 wp_read.
+    - iDestruct "big" as "(↦tl & ↦tys & ex†)". wp_read. wp_op. do 2 wp_read.
       do 2 wp_op. wp_write. do 2 rewrite -{1}heap_mapsto_vec_singleton.
       rewrite !freeable_sz_full. wp_bind (delete _).
       iApply (wp_delete with "[$↦v $†v]"); [done|].
@@ -219,9 +219,8 @@ Section smallvec_index.
           by iApply proph_eqz_vinsert. }
         rewrite split_mt_smallvec. iExists false, _, _, _, _=>/=.
         rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
-        iFrame "↦₀ ↦₁ ↦₂ ↦₃ ex†". iSplit; [by rewrite vec_to_list_apply|].
-        iClear "#". iExists _. iFrame "↦tl". iSplit; [done|].
-        rewrite vinsert_backmid -big_sepL_vbackmid Eqi. iSplitL "↦tys".
+        iFrame "↦₀ ↦₁ ↦₂ ↦₃ ↦tl ex†". iSplit; [by rewrite vec_to_list_apply|].
+        iClear "#". rewrite vinsert_backmid -big_sepL_vbackmid Eqi. iSplitL "↦tys".
         { iStopProof. do 6 f_equiv. iApply ty_own_depth_mono. lia. }
         setoid_rewrite shift_loc_assoc. iSplitL "↦ty".
         { iStopProof. do 3 f_equiv. iApply ty_own_depth_mono. lia. }
diff --git a/theories/typing/lib/smallvec/smallvec_pop.v b/theories/typing/lib/smallvec/smallvec_pop.v
index ff65b19cd29fa819a1fc607897fecb9f1150a285..8341a4ca45d236d6e9f4817b45abe9e8a342e507 100644
--- a/theories/typing/lib/smallvec/smallvec_pop.v
+++ b/theories/typing/lib/smallvec/smallvec_pop.v
@@ -42,8 +42,7 @@ Section smallvec_pop.
     iDestruct "uniq" as (d ξi [? Eq2]) "[Vo Bor]". move: Eq2. set ξ := PrVar _ ξi=> Eq2.
     iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
     iMod (bor_acc with "LFT Bor α") as "[(%&%& #⧖ & Pc & big) ToBor]"; [done|].
-    wp_seq. iDestruct (uniq_agree with "Vo Pc") as %[<-<-].
-    rewrite split_mt_smallvec.
+    wp_seq. iDestruct (uniq_agree with "Vo Pc") as %[<-<-]. rewrite split_mt_smallvec.
     iDestruct "big" as (?? len ex aπl Eq1) "(↦ & big)".
     rewrite !heap_mapsto_vec_cons !shift_loc_assoc.
     iDestruct "↦" as "(↦₀ & ↦₁ & ↦₂ & ↦₃ &_)". wp_op. wp_read. wp_let.
@@ -106,7 +105,7 @@ Section smallvec_pop.
         { inv_vec aπl=> + aπl'. by elim aπl'=>/= *. }
         have ->: removelast (lapply aπl π) = lapply (vinit aπl) π.
         { inv_vec aπl=> + aπl'. elim aπl'; [done|]=>/= *. by f_equal. } done.
-    - iDestruct "big" as (??) "(↦tl & ↦tys & (%&% & ↦ex) & †)".
+    - iDestruct "big" as "(↦tl & ↦tys & (%&% & ↦ex) & †)".
       iDestruct (big_sepL_vinitlast with "↦tys") as "[↦tys (%& ↦last & ty)]"=>/=.
       iDestruct (ty_size_eq with "ty") as %Lvl. do 2 wp_op. wp_read. wp_op.
       wp_write. have ->: (ex + 1)%Z = S ex by lia. do 2 wp_op. wp_read.
@@ -117,10 +116,9 @@ Section smallvec_pop.
       { iNext. iExists _, _. iFrame "⧖ Pc". rewrite split_mt_smallvec.
         iExists _, _, _, _, _.
         rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
-        iFrame "↦₀ ↦₁ ↦₂ ↦₃ ↦tys". iSplit; [done|]. iExists _. iFrame "↦tl".
-        iSplit; [done|]. have ->: len + S ex = S (len + ex) by lia. iFrame "†".
-        iExists (_++_). rewrite heap_mapsto_vec_app. iFrame "↦last".
-        rewrite shift_loc_assoc_nat app_length Nat.add_comm Lvl.
+        iFrame "↦₀ ↦₁ ↦₂ ↦₃ ↦tl ↦tys". have ->: len + S ex = S (len + ex) by lia.
+        iFrame "†". iSplit; [done|]. iExists (_++_). rewrite heap_mapsto_vec_app.
+        iFrame "↦last". rewrite shift_loc_assoc_nat app_length Nat.add_comm Lvl.
         iFrame. iPureIntro=>/=. lia. }
       iMod ("ToL" with "α L") as "L".
       iApply (type_type +[#v' ◁ &uniq{α} (smallvec n ty); #r ◁ box (option_ty ty)]
diff --git a/theories/typing/lib/smallvec/smallvec_push.v b/theories/typing/lib/smallvec/smallvec_push.v
index ab3edd2accb57bcb8603f86344ddcc8937039ad8..c830ac54340e8075d06b78256990d54eed1bdf79 100644
--- a/theories/typing/lib/smallvec/smallvec_push.v
+++ b/theories/typing/lib/smallvec/smallvec_push.v
@@ -35,7 +35,7 @@ Section smallvec_push.
     rewrite split_mt_smallvec. iDestruct "big" as (b ? len ??->) "(↦ & big)".
     rewrite heap_mapsto_vec_cons. iDestruct "↦" as "[↦₀ ↦']". wp_rec. wp_read.
     wp_if. case b=>/=; last first.
-    { iDestruct "big" as (??) "(↦tl & ↦tys & ↦ex & †)". wp_op.
+    { iDestruct "big" as "((%&%& ↦tl) & ↦tys & ↦ex & †)". wp_op.
       iApply (wp_vec_push_core with "[↦' ↦tys ↦ex † ↦x ty]").
       { iExists _, _. iFrame "↦' † ↦ex ↦tys". iExists _. iFrame. }
       iIntros "!> (%&%& ↦' & ↦tys & ↦ex & † & ↦x)". iApply "ToΦ". iFrame "↦x".
@@ -82,10 +82,10 @@ Section smallvec_push.
       rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
       iFrame "↦₀ ↦₁ ↦₂ ↦₃"=>/=. iSplit.
       { iPureIntro. fun_ext=> ?. by rewrite vec_to_list_snoc lapply_app. }
-      iExists (_++_). rewrite EqLen app_length heap_mapsto_vec_app shift_loc_assoc.
-      iFrame "↦o". rewrite Lwll. iFrame "↦tl". rewrite Nat.add_comm Nat.add_0_r.
-      iFrame "†". iSplit; [done|]. iSplitL; last first.
-      { iExists []. by rewrite heap_mapsto_vec_nil. }
+      rewrite Nat.add_comm Nat.add_0_r. iFrame "†". iSplitL "↦o ↦tl".
+      { iExists (_++_). rewrite EqLen app_length heap_mapsto_vec_app shift_loc_assoc.
+        iFrame "↦o". rewrite Lwll. by iFrame "↦tl". }
+      iSplitL; last first. { iExists []. by rewrite heap_mapsto_vec_nil. }
       rewrite vec_to_list_snoc big_sepL_app big_sepL_singleton. iSplitL "tys ↦l".
       + rewrite trans_big_sepL_mt_ty_own. iExists _. iFrame "↦l". iStopProof.
         do 3 f_equiv. apply ty_own_depth_mono. lia.
diff --git a/theories/typing/lib/smallvec/smallvec_slice.v b/theories/typing/lib/smallvec/smallvec_slice.v
index 6eb6daae501f2e03abe92bb9c4170b552ce73c2b..f27c7dc490a18e31d94510759d2edf3332dccd1b 100644
--- a/theories/typing/lib/smallvec/smallvec_slice.v
+++ b/theories/typing/lib/smallvec/smallvec_slice.v
@@ -76,7 +76,7 @@ Section smallvec_slice.
           iApply proph_eqz_constr. iApply (proph_eqz_prvars with "Eqzs"). }
         rewrite split_mt_smallvec. iExists true, _, _, _, _=>/=.
         rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc. by iFrame.
-    - iDestruct "big" as (??) "(↦tl & ↦tys & †)". wp_op. wp_read. wp_write. do 2 wp_seq.
+    - iDestruct "big" as "(↦tl & ↦tys & †)". wp_op. wp_read. wp_write. do 2 wp_seq.
       iMod ("ToBor" $! (big_sepL _ _) with "[↦₀ ↦₁ ↦₂ ↦₃ ↦tl † ToPc] [↦tys Pcs]")
         as "[Bor α]"; last first.
       + iMod ("ToL" with "α L") as "L". rewrite cctx_interp_singleton.
@@ -99,7 +99,6 @@ Section smallvec_slice.
         { iApply "ToPc". rewrite -!vec_to_list_apply.
           iApply proph_eqz_constr. iApply (proph_eqz_prvars with "Eqzs"). }
         rewrite split_mt_smallvec. iExists false, _, _, _, _=>/=.
-        rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
-        iFrame "↦₀ ↦₁ ↦₂ ↦₃ †". iSplit; [done|]. iExists _. by iFrame.
+        rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc. by iFrame.
   Qed.
 End smallvec_slice.