diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 47e683ad9d02c37f2ae1efe4b4fb2a0bcad0dbbe..23666066549dce29bde5870b4e4dca3ceefad7e8 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -336,13 +336,11 @@ Section cell.
     iIntros (?[vπ[]]?) "LFT _ PROPH UNIQ E Na L C /=[x _] Obs".
     rewrite tctx_hasty_val. iDestruct "x" as ([|]) "[_ box]"=>//.
     case x as [[|x|]|]=>//. iDestruct "box" as "[(%& ↦x & [_ uniq]) †x]".
-    wp_bind (new _). iApply wp_new; [done..|]. iIntros "!>" (?) "[†r ↦r]".
-    wp_seq. case vl as [|[[]|][]]=>//.
+    wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]". wp_seq. case vl as [|[[]|][]]=>//.
     iDestruct "uniq" as (? i [? Eq']) "[Vo Bor]". set ξ := PrVar _ i.
     iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
-    iMod (bor_acc with "LFT Bor α") as "[big Toα]"; [done|]. wp_bind (delete _).
-    rewrite freeable_sz_full. iApply (wp_delete with "[$↦x $†x]"); [done|].
-    iIntros "!> _". do 3 wp_seq.
+    iMod (bor_acc with "LFT Bor α") as "[big Toα]"; [done|]. rewrite freeable_sz_full.
+    wp_apply (wp_delete with "[$↦x $†x]"); [done|]. iIntros "_". do 3 wp_seq.
     iDestruct "big" as (??) "(_& Pc &%& ↦ &%&%&%&->& Obs' & #⧖ & ty)".
     iDestruct (uniq_agree with "Vo Pc") as %[Eq <-].
     iMod (uniq_update ξ (const Φ) with "UNIQ Vo Pc") as "[Vo Pc]"; [done|].
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 8d360678e0de50f28cf792a5b1899d10ec043d90..66ebcb7d65f428ed92243337aa6129adfde9817a 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -169,15 +169,13 @@ Section mutex.
     iIntros (?[?[]]?) "_ _ _ _ _ Na L C /=[x _] #Obs".
     rewrite tctx_hasty_val. iDestruct "x" as ([|]) "[#⧖ box]"=>//.
     case x as [[|x|]|]=>//=. iDestruct "box" as "[(%& >↦x & ty) †x]".
-    wp_bind (new _). iApply wp_new; [done..|]. iIntros "!> % [†m ↦m]".
+    wp_apply wp_new; [done..|]. iIntros (?) "[†m ↦m]".
     iDestruct (ty_size_eq with "ty") as %Szvl.
-    rewrite Nat2Z.id /= heap_mapsto_vec_cons. iDestruct "↦m" as "[↦b ↦m]".
-    wp_let. wp_op. wp_bind (_ <-{_} !_)%E.
-    iApply (wp_memcpy with "[$↦m $↦x]"); [by rewrite repeat_length|lia|].
-    iIntros "!> [↦m ↦x]". wp_seq. wp_op. rewrite shift_loc_0. wp_rec. wp_write.
-    wp_bind (delete _). iApply (wp_delete with "[$↦x †x]"); [lia| |].
-    { by rewrite freeable_sz_full Szvl. }
-    iIntros "!>_". do 3 wp_seq. rewrite cctx_interp_singleton.
+    rewrite Nat2Z.id /= heap_mapsto_vec_cons. iDestruct "↦m" as "[↦b ↦m]". wp_let.
+    wp_op. wp_apply (wp_memcpy with "[$↦m $↦x]"); [by rewrite repeat_length|lia|].
+    iIntros "[↦m ↦x]". wp_seq. wp_op. rewrite shift_loc_0. wp_rec. wp_write.
+    wp_apply (wp_delete with "[$↦x †x]"); [lia| |]. { by rewrite freeable_sz_full Szvl. }
+    iIntros "_". do 3 wp_seq. rewrite cctx_interp_singleton.
     iApply ("C" $! [# #_] -[const Φ] with "Na L [-] []"); last first.
     { by iApply proph_obs_impl; [|done]=>/= ?[_ ?]. }
     rewrite/= right_id (tctx_hasty_val #_). iExists _. iFrame "⧖".
@@ -200,16 +198,14 @@ Section mutex.
     eapply type_fn; [apply _|]=>/= _ ??[m[]]. simpl_subst.
     iIntros (?[?[]]?) "_ _ _ _ _ Na L C /=[m _] Obs". rewrite tctx_hasty_val.
     iDestruct "m" as ([|]) "[_ box]"=>//. case m as [[|m|]|]=>//=.
-    rewrite split_mt_mutex. iDestruct "box" as "[↦mtx †m]". wp_bind (new _).
-    iApply wp_new; [lia|done|]. rewrite Nat2Z.id. iIntros "!>% [†x ↦x]". wp_let.
-    iDestruct "↦mtx" as (????->) "(↦b & Obs' & ⧖ &%& ↦m & ty)".
-    iCombine "Obs Obs'" as "#?". iDestruct (ty_size_eq with "ty") as %Szvl.
-    wp_op. wp_bind (_ <-{_} !_)%E.
-    iApply (wp_memcpy with "[$↦x $↦m]"); [|lia|]. { by rewrite repeat_length. }
-    iIntros "!> [↦x ↦m]". wp_seq. wp_bind (delete _).
-    iApply (wp_delete (_::_) with "[↦b ↦m †m]"); swap 1 2.
+    rewrite split_mt_mutex. iDestruct "box" as "[↦mtx †m]".
+    wp_apply wp_new; [lia|done|]. rewrite Nat2Z.id. iIntros (?) "[†x ↦x]".
+    wp_let. iDestruct "↦mtx" as (????->) "(↦b & Obs' & ⧖ &%& ↦m & ty)".
+    iCombine "Obs Obs'" as "#?". iDestruct (ty_size_eq with "ty") as %Szvl. wp_op.
+    wp_apply (wp_memcpy with "[$↦x $↦m]"); [|lia|]. { by rewrite repeat_length. }
+    iIntros "[↦x ↦m]". wp_seq. wp_apply (wp_delete (_::_) with "[↦b ↦m †m]"); swap 1 2.
     { rewrite heap_mapsto_vec_cons freeable_sz_full -Szvl. iFrame. } { simpl. lia. }
-    iIntros "!>_". do 3 wp_seq. rewrite cctx_interp_singleton.
+    iIntros "_". do 3 wp_seq. rewrite cctx_interp_singleton.
     iApply ("C" $! [# #_] -[_] with "Na L [-]"); last first.
     { iApply proph_obs_impl; [|done]=>/= ?[Imp ?]. by apply Imp. }
     rewrite/= right_id (tctx_hasty_val #_). iExists _. iFrame "⧖".
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index ee2ba7b68f50b1524416c8be5cdd169ef51aedd6..ff8809060912a1f16b77f41786baa8a7e25d3b91 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -205,10 +205,10 @@ Section mutexguard.
     iDestruct "↦mtx" as (?) "(↦m &%&%&>->& ? & ? & #At)". wp_read. wp_let.
     iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
     wp_apply (acquire_spec with "[] α"). { by iApply (mutex_acc with "LFT At"). }
-    iIntros "[Bor α]". wp_seq. wp_bind (new _). iApply wp_new; [done..|].
-    iIntros "!>% [†g ↦g]". wp_let. rewrite heap_mapsto_vec_singleton. wp_write.
-    wp_bind (delete _). rewrite -heap_mapsto_vec_singleton freeable_sz_full.
-    iApply (wp_delete with "[$↦m $†m]"); [done|]. iIntros "!>_". do 3 wp_seq.
+    iIntros "[Bor α]". wp_seq. wp_apply wp_new; [done..|]. iIntros (?) "[†g ↦g]".
+    wp_let. rewrite heap_mapsto_vec_singleton. wp_write.
+    rewrite -heap_mapsto_vec_singleton freeable_sz_full.
+    wp_apply (wp_delete with "[$↦m $†m]"); [done|]. iIntros "_". do 3 wp_seq.
     iMod ("ToL" with "α L") as "L". rewrite cctx_interp_singleton.
     iApply ("C" $! [# #_] -[_] with "Na L [-] Obs").
     rewrite/= right_id (tctx_hasty_val #_). iExists _. iSplit; [done|].
@@ -256,7 +256,7 @@ Section mutexguard.
     iMod (bor_sep_persistent with "LFT Bor α") as "(#β⊑κ & Bor & α)"; [done|].
     do 2 (iMod (bor_sep with "LFT Bor") as "[_ Bor]"; [done|]).
     iMod (bor_unnest with "LFT Bor") as "Bor"; [done|]. wp_let. iMod "Bor".
-    wp_bind (new _). iApply wp_new; [done..|]. iIntros "!>% [†r ↦r]".
+    wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]".
     set κ' := _ ⊓ α. iAssert (α ⊑ κ')%I as "#α⊑κ'".
     { iApply lft_incl_glb; [|iApply lft_incl_refl]. iApply lft_incl_trans; [|done].
       iApply lft_incl_trans; [done|]. iApply lft_intersect_incl_l. }
@@ -343,7 +343,7 @@ Section mutexguard.
     iIntros "α". wp_seq. iMod ("ToL" with "α L") as "L". wp_bind (delete _).
     rewrite -heap_mapsto_vec_singleton freeable_sz_full.
     iApply (wp_delete with "[$↦g $†g]"); [done|]. iIntros "!>_". do 3 wp_seq.
-    wp_bind (new _). iApply wp_new; [done..|]. iIntros "!>% [†r ↦r]".
+    wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]".
     rewrite cctx_interp_singleton. iApply ("C" $! [# #_] -[_] with "Na L [-] Obs").
     rewrite/= right_id (tctx_hasty_val #_). iExists _. iSplit; [done|].
     rewrite -freeable_sz_full. iFrame "†r". iNext. iExists _. iFrame "↦r".
diff --git a/theories/typing/lib/smallvec/smallvec.v b/theories/typing/lib/smallvec/smallvec.v
index 135a923ac5af603e70dbed3e2d3595fe87e65bcd..520748e5ac2dac95c7df3ea1ecdf6b0cb61afc3c 100644
--- a/theories/typing/lib/smallvec/smallvec.v
+++ b/theories/typing/lib/smallvec/smallvec.v
@@ -30,9 +30,6 @@ Notation "if@ b 'then' P 'else' Q" := (choice b P Q) (at level 200,
 Section smallvec.
   Context `{!typeG Σ}.
 
-  Global Instance loc_inhabited : Inhabited loc := populate (inhabitant, inhabitant).
-  Definition any_loc: loc := inhabitant.
-
   Lemma split_mt_smallvec {𝔄} (ty: type 𝔄) k l' tid d alπ Φ :
     (l' ↦∗: (λ vl,
       ∃(b: bool) (l: loc) (len ex: nat) wl (aπl: vec (proph 𝔄) len),
diff --git a/theories/typing/lib/smallvec/smallvec_basic.v b/theories/typing/lib/smallvec/smallvec_basic.v
index 9515cde6c5c4110471f5c636d1a0db561c2dd0c2..08fce15653e9dcb4e7c6b0d6e589813d348dceb2 100644
--- a/theories/typing/lib/smallvec/smallvec_basic.v
+++ b/theories/typing/lib/smallvec/smallvec_basic.v
@@ -100,7 +100,7 @@ Section smallvec_basic.
   Definition smallvec_new {𝔄} n (ty: type 𝔄): val :=
     fn: [] :=
       let: "r" := new [ #((4 + n * ty.(ty_size))%nat)] in
-      "r" <- #true;; "r" +ₗ #1 <- #any_loc;;
+      "r" <- #true;; "r" +ₗ #1 <- #(inhabitant: loc);;
       "r" +ₗ #2 <- #0;; "r" +ₗ #3 <- #0;;
       return: ["r"].
 
@@ -117,10 +117,10 @@ Section smallvec_basic.
     do 3 (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. iFrame "↦₀ ↦₁ ↦₂ ↦₃ ↦ex".
-    iExists true, _, 0, 0, (repeat _ _), [#]. rewrite/= repeat_length.
-    iSplit; [done|]. by iExists [#], _=>/=.
+    iFrame "†". iNext. rewrite split_mt_smallvec. iExists true, _, 0, 0, [#].
+    rewrite/= !heap_mapsto_vec_cons !shift_loc_assoc heap_mapsto_vec_nil.
+    iFrame "↦₀ ↦₁ ↦₂ ↦₃". do 2 (iSplit; [done|]). iExists _. iFrame.
+    by rewrite repeat_length.
   Qed.
 
   Definition smallvec_delete {𝔄} n (ty: type 𝔄) : val :=
@@ -147,14 +147,13 @@ Section smallvec_basic.
     - rewrite trans_big_sepL_mt_ty_own.
       iDestruct "big" as "[(%wll & ↦ar & tys) (%wl' & -> & ↦ex)]".
       iDestruct (big_sepL_ty_own_length with "tys") as %<-. rewrite -app_length.
-      wp_bind (delete _).
-      iApply (wp_delete (_::_::_::_::_) with "[↦₀ ↦₁ ↦₂ ↦₃ ↦ar ↦ex †]"); [done|..].
+      wp_apply (wp_delete (_::_::_::_::_) with "[↦₀ ↦₁ ↦₂ ↦₃ ↦ar ↦ex †]"); [done|..].
       { rewrite !heap_mapsto_vec_cons heap_mapsto_vec_app !shift_loc_assoc
           freeable_sz_full. iFrame. }
-      iIntros "!>_". wp_seq. iMod persistent_time_receipt_0 as "⧖".
+      iIntros "_". wp_seq. iMod persistent_time_receipt_0 as "⧖".
       wp_bind Skip. iApply (wp_persistent_time_receipt with "TIME ⧖"); [done|].
-      wp_seq. iIntros "⧖". wp_seq. wp_bind (new _). iApply wp_new; [done..|].
-      iIntros "!>" (?) "[† ↦]". rewrite cctx_interp_singleton.
+      wp_seq. iIntros "⧖". wp_seq. wp_apply wp_new; [done..|].
+      iIntros (?) "[† ↦]". rewrite cctx_interp_singleton.
       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.
@@ -163,15 +162,14 @@ Section smallvec_basic.
       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.
-      wp_bind (delete _). iApply (wp_delete (_++_) with "[↦ar ↦ex †']"); [done|..].
-      { rewrite heap_mapsto_vec_app. iFrame. }
-      iIntros "!>_". wp_seq. wp_bind (delete _).
-      iApply (wp_delete (_::_::_::_::_) with "[↦₀ ↦₁ ↦₂ ↦₃ ↦tl †]"); [done| |].
+      wp_apply (wp_delete (_++_) with "[↦ar ↦ex †']"); [done|..].
+      { rewrite heap_mapsto_vec_app. iFrame. } iIntros "_". wp_seq.
+      wp_apply (wp_delete (_::_::_::_::_) with "[↦₀ ↦₁ ↦₂ ↦₃ ↦tl †]"); [done| |].
       { rewrite !heap_mapsto_vec_cons !shift_loc_assoc freeable_sz_full. iFrame. }
-      iIntros "!>_". wp_seq. iMod persistent_time_receipt_0 as "⧖".
+      iIntros "_". wp_seq. iMod persistent_time_receipt_0 as "⧖".
       wp_bind Skip. iApply (wp_persistent_time_receipt with "TIME ⧖"); [done|].
-      wp_seq. iIntros "⧖". wp_seq. wp_bind (new _). iApply wp_new; [done..|].
-      iIntros "!>" (?) "[† ↦]". rewrite cctx_interp_singleton.
+      wp_seq. iIntros "⧖". wp_seq. wp_apply wp_new; [done..|].
+      iIntros (?) "[† ↦]". rewrite cctx_interp_singleton.
       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.
diff --git a/theories/typing/lib/smallvec/smallvec_index.v b/theories/typing/lib/smallvec/smallvec_index.v
index fb0d6fb02cbe7c9862897a54a096b334d58de5bc..216d40338e1a2897d7081480bb90317d76394101 100644
--- a/theories/typing/lib/smallvec/smallvec_index.v
+++ b/theories/typing/lib/smallvec/smallvec_index.v
@@ -31,7 +31,7 @@ Section smallvec_index.
     rewrite !tctx_hasty_val.
     iDestruct "v" as ([|d]) "[⧖ v]"=>//. case v as [[|v|]|]=>//=.
     iDestruct "i" as ([|]) "[_ i]"=>//. case i as [[|i|]|]=>//=.
-    wp_bind (new _). iApply wp_new; [done..|]. iIntros "!>% [†r ↦r]". wp_let.
+    wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]". wp_let.
     iDestruct "v" as "[(%vl & ↦v & svec) †v]". move: d=> [|d]//=.
     case vl as [|[[]|][]]=>//. iDestruct "svec" as (?????->) "[Bor tys]".
     iDestruct "i" as "[(%& ↦i & (%&->&->)) †i]"=>/=.
@@ -42,9 +42,8 @@ Section smallvec_index.
     - wp_read. wp_op. wp_read. do 2 wp_op. wp_write.
       iMod ("Toα" with "[$↦₀ $↦₁ $↦₂ $↦₃]") as "α". iMod ("ToL" with "α L") as "L".
       do 2 rewrite -heap_mapsto_vec_singleton freeable_sz_full.
-      wp_bind (delete _). iApply (wp_delete with "[$↦v $†v]"); [done|].
-      iIntros "!> _". wp_seq. wp_bind (delete _).
-      iApply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "!> _". do 3 wp_seq.
+      wp_apply (wp_delete with "[$↦v $†v]"); [done|]. iIntros "_". wp_seq.
+      wp_apply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "_". do 3 wp_seq.
       iMod (proph_obs_sat with "PROPH Obs") as %(?& inat &?&->& Lkup &_); [done|].
       move: Lkup. rewrite -vec_to_list_apply -vlookup_lookup'. move=> [In _].
       set ifin := nat_to_fin In. have Eqi: inat = ifin by rewrite fin_to_nat_to_fin.
@@ -60,9 +59,8 @@ Section smallvec_index.
     - wp_read. wp_op. do 2 wp_read. do 2 wp_op. wp_write.
       iMod ("Toα" with "[$↦₀ $↦₁ $↦₂ $↦₃]") as "α". iMod ("ToL" with "α L") as "L".
       do 2 rewrite -heap_mapsto_vec_singleton freeable_sz_full.
-      wp_bind (delete _). iApply (wp_delete with "[$↦v $†v]"); [done|].
-      iIntros "!> _". wp_seq. wp_bind (delete _).
-      iApply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "!> _". do 3 wp_seq.
+      wp_apply (wp_delete with "[$↦v $†v]"); [done|]. iIntros "_". wp_seq.
+      wp_apply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "_". do 3 wp_seq.
       iMod (proph_obs_sat with "PROPH Obs") as %(?& inat &?&->& Lkup &_); [done|].
       move: Lkup. rewrite -vec_to_list_apply -vlookup_lookup'. move=> [In _].
       set ifin := nat_to_fin In. have Eqi: inat = ifin by rewrite fin_to_nat_to_fin.
@@ -88,7 +86,7 @@ Section smallvec_index.
     rewrite !tctx_hasty_val.
     iDestruct "v" as ([|d]) "[#⧖ v]"=>//. case v as [[|v|]|]=>//=.
     iDestruct "i" as ([|]) "[_ i]"=>//. case i as [[|i|]|]=>//=.
-    wp_bind (new _). iApply wp_new; [done..|]. iIntros "!>% [†r ↦r]".
+    wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]".
     iDestruct "v" as "[(%vl & ↦v & #In & uniq) †v]". case vl as [|[[]|][]]=>//=.
     iDestruct "i" as "[(%& ↦i & (%&->&->)) †i]". rewrite !heap_mapsto_vec_singleton.
     iDestruct "uniq" as (d' ξi [Le Eq2]) "[Vo Bor]". set ξ := PrVar _ ξi.
@@ -104,9 +102,8 @@ Section smallvec_index.
     do 2 wp_read. case b; wp_case.
     - iDestruct "big" as "[↦tys ↦tl]". wp_read. wp_op. 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|].
-      iIntros "!>_". wp_seq. wp_bind (delete _).
-      iApply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "!>_". wp_seq.
+      wp_apply (wp_delete with "[$↦v $†v]"); [done|]. iIntros "_". wp_seq.
+      wp_apply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "_". wp_seq.
       iMod (proph_obs_sat with "PROPH Obs") as %(?& Obs); [done|].
       move: Obs=> [inat[?[->[+ _]]]]. rewrite -vec_to_list_apply -vlookup_lookup'.
       move=> [In _]. rewrite -Nat2Z.inj_mul. set ifin := nat_to_fin In.
@@ -165,11 +162,9 @@ Section smallvec_index.
         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.
       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|].
-      iIntros "!>_". wp_seq. wp_bind (delete _).
-      iApply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "!>_". wp_seq.
-      iMod (proph_obs_sat with "PROPH Obs") as %(?& Obs); [done|].
+      rewrite !freeable_sz_full. wp_apply (wp_delete with "[$↦v $†v]"); [done|].
+      iIntros "_". wp_seq. wp_apply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "_".
+      wp_seq. iMod (proph_obs_sat with "PROPH Obs") as %(?& Obs); [done|].
       move: Obs=> [inat[?[->[+ _]]]]. rewrite -vec_to_list_apply -vlookup_lookup'.
       move=> [In _]. rewrite -Nat2Z.inj_mul. set ifin := nat_to_fin In.
       have Eqi: inat = ifin by rewrite fin_to_nat_to_fin.
diff --git a/theories/typing/lib/smallvec/smallvec_pop.v b/theories/typing/lib/smallvec/smallvec_pop.v
index 8341a4ca45d236d6e9f4817b45abe9e8a342e507..a5c1c4e86e50a372b5f3bbfd81a320f4680e8683 100644
--- a/theories/typing/lib/smallvec/smallvec_pop.v
+++ b/theories/typing/lib/smallvec/smallvec_pop.v
@@ -36,9 +36,9 @@ Section smallvec_pop.
     rewrite tctx_hasty_val. iDestruct "v" as ([|]) "[_ v]"=>//.
     case v as [[|v|]|]=>//. iDestruct "v" as "[(%vl & >↦ & [#LftIn uniq]) †]".
     case vl as [|[[|v'|]|][]]; try by iDestruct "uniq" as ">[]".
-    rewrite heap_mapsto_vec_singleton. wp_read. wp_let. wp_bind (delete _).
+    rewrite heap_mapsto_vec_singleton. wp_read. wp_let.
     rewrite -heap_mapsto_vec_singleton freeable_sz_full.
-    iApply (wp_delete with "[$↦ $†]"); [done|]. iIntros "!>_".
+    wp_apply (wp_delete with "[$↦ $†]"); [done|]. iIntros "_".
     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|].
diff --git a/theories/typing/lib/smallvec/smallvec_push.v b/theories/typing/lib/smallvec/smallvec_push.v
index c830ac54340e8075d06b78256990d54eed1bdf79..e1981f5f142659ccda592f12b57d98156be5aa0c 100644
--- a/theories/typing/lib/smallvec/smallvec_push.v
+++ b/theories/typing/lib/smallvec/smallvec_push.v
@@ -67,16 +67,16 @@ Section smallvec_push.
       + iExists _. iSplitL "↦new".
         * rewrite vec_to_list_length Nat.add_0_r shift_loc_assoc. iFrame.
         * iApply ty_own_depth_mono; [|done]. lia.
-    - do 2 wp_op. wp_bind (new _). iApply wp_new; [lia|done|]. iIntros "!>% [† ↦l]".
+    - do 2 wp_op. wp_apply wp_new; [lia|done|]. iIntros (?) "[† ↦l]".
       have ->: ∀sz: nat, ((len + 1) * sz)%Z = len * sz + sz by lia.
-      rewrite Nat2Z.id. wp_let. do 2 wp_op. wp_bind (memcpy _).
+      rewrite Nat2Z.id. wp_let. do 2 wp_op.
       rewrite repeat_app heap_mapsto_vec_app. iDestruct "↦l" as "[↦l ↦new]".
       rewrite repeat_length trans_big_sepL_mt_ty_own. iDestruct "↦tys" as (?) "[↦o tys]".
       iDestruct (big_sepL_ty_own_length with "tys") as %Lwll.
-      iApply (wp_memcpy with "[$↦l $↦o]"); [rewrite repeat_length; lia|lia|].
-      iIntros "!>[↦l ↦o]". wp_seq. do 2 wp_op. rewrite -Nat2Z.inj_mul. wp_bind (memcpy _).
-      iApply (wp_memcpy with "[$↦new $↦x]"); [by rewrite repeat_length|lia|].
-      iIntros "!>[↦new ↦x]". wp_seq. wp_write. do 2 (wp_op; wp_write).
+      wp_apply (wp_memcpy with "[$↦l $↦o]"); [rewrite repeat_length; lia|lia|].
+      iIntros "[↦l ↦o]". wp_seq. do 2 wp_op. rewrite -Nat2Z.inj_mul.
+      wp_apply (wp_memcpy with "[$↦new $↦x]"); [by rewrite repeat_length|lia|].
+      iIntros "[↦new ↦x]". wp_seq. wp_write. do 2 (wp_op; wp_write).
       iApply "ToΦ". iSplitR "↦x"; last first. { iExists _. by iFrame. }
       rewrite split_mt_smallvec. iExists _, _, _, 0, (vsnoc _ _).
       rewrite !heap_mapsto_vec_cons heap_mapsto_vec_nil !shift_loc_assoc.
@@ -116,13 +116,13 @@ Proof.
     iMod (lctx_lft_alive_tok α with "E L") as (?) "(α & L & ToL)"; [solve_typing..|].
     iMod (bor_acc with "LFT Bor α") as "[(%&%& ⧖u & Pc & ↦sv) ToBor]"; [done|].
     wp_seq. iDestruct (uniq_agree with "Vo Pc") as %[<-<-].
-    wp_bind (delete _). rewrite -heap_mapsto_vec_singleton freeable_sz_full.
-    iApply (wp_delete with "[$↦v $†v]"); [done|]. iCombine "⧖u ⧖x" as "#⧖".
-    iIntros "!>_". wp_seq. wp_bind (smallvec_push_core _ _ _).
-    iApply (wp_smallvec_push_core with "[$↦sv $↦ty]").
-    iIntros "!>[↦sv (%& %Lvl & ↦x)]". wp_seq. rewrite freeable_sz_full.
-    wp_bind (delete _). iApply (wp_delete with "[$↦x †x]"); [lia|by rewrite Lvl|].
-    iIntros "!>_". wp_seq. set pπ' := λ π, ((pπ π).1 ++ [bπ π], π ξ).
+    rewrite -heap_mapsto_vec_singleton freeable_sz_full.
+    wp_apply (wp_delete with "[$↦v $†v]"); [done|]. iIntros "_".
+    iCombine "⧖u ⧖x" as "#⧖". wp_seq.
+    wp_apply (wp_smallvec_push_core with "[$↦sv $↦ty]").
+    iIntros "[↦sv (%& %Lvl & ↦x)]". wp_seq. rewrite freeable_sz_full.
+    wp_apply (wp_delete with "[$↦x †x]"); [lia|by rewrite Lvl|]. iIntros "_".
+    wp_seq. set pπ' := λ π, ((pπ π).1 ++ [bπ π], π ξ).
     iMod (uniq_update with "UNIQ Vo Pc") as "[Vo Pc]"; [done|].
     iMod ("ToBor" with "[Pc ↦sv]") as "[Bor α]". { iExists _, _. iFrame "⧖ Pc ↦sv". }
     iMod ("ToL" with "α L") as "L".
diff --git a/theories/typing/lib/vec/vec_basic.v b/theories/typing/lib/vec/vec_basic.v
index 8cfd4b837862b59803ccdc046d542caf9d5b0507..29b2742fd2befe97193c82994f14969f27488f3a 100644
--- a/theories/typing/lib/vec/vec_basic.v
+++ b/theories/typing/lib/vec/vec_basic.v
@@ -87,7 +87,7 @@ Section vec_basic.
   Proof.
     eapply type_fn; [apply _|]=> _ ???. simpl_subst.
     iIntros (???) "_ #TIME _ _ _ Na L C _ Obs".
-    wp_bind (new _). iApply wp_new; [done..|]. iIntros "!>" (r).
+    wp_apply wp_new; [done..|]. iIntros (r).
     rewrite !heap_mapsto_vec_cons shift_loc_assoc. iIntros "[† (↦₀ & ↦₁ & ↦₂ &_)]".
     wp_seq. iMod persistent_time_receipt_0 as "⧖". wp_bind (new _).
     iApply (wp_persistent_time_receipt with "TIME ⧖"); [done|].
@@ -124,16 +124,15 @@ Section vec_basic.
     iDestruct "big" as "((%& ↦old & tys) & (%& %Eq & ↦ex) & †')".
     iDestruct (big_sepL_ty_own_length with "tys") as %Eq'.
     rewrite -Nat2Z.inj_add -Nat2Z.inj_mul !Nat.mul_add_distr_r -Eq -Eq' -app_length.
-    wp_bind (delete _). iApply (wp_delete (_++_) with "[↦old ↦ex †']"); [done|..].
+    wp_apply (wp_delete (_++_) with "[↦old ↦ex †']"); [done|..].
     { rewrite heap_mapsto_vec_app app_length. iFrame. }
-    iIntros "!>_". wp_seq. wp_bind (delete _).
-    iApply (wp_delete [_;_;_] with "[↦₀ ↦₁ ↦₂ †]"); [done| |].
+    iIntros "_". wp_seq. wp_apply (wp_delete [_;_;_] with "[↦₀ ↦₁ ↦₂ †]"); [done| |].
     { rewrite !heap_mapsto_vec_cons shift_loc_assoc heap_mapsto_vec_nil
         freeable_sz_full. iFrame. }
-    iIntros "!>_". wp_seq. iMod persistent_time_receipt_0 as "⧖".
+    iIntros "_". wp_seq. iMod persistent_time_receipt_0 as "⧖".
     wp_bind Skip. iApply (wp_persistent_time_receipt with "TIME ⧖"); [done|].
-    wp_seq. iIntros "⧖". wp_seq. wp_bind (new _). iApply wp_new; [done..|].
-    iIntros "!>" (?) "[† ↦]". rewrite cctx_interp_singleton.
+    wp_seq. iIntros "⧖". wp_seq. wp_apply wp_new; [done..|].
+    iIntros (?) "[† ↦]". rewrite cctx_interp_singleton.
     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.
diff --git a/theories/typing/lib/vec/vec_index.v b/theories/typing/lib/vec/vec_index.v
index 0a30617f9df3133859f308695a1cb87be5664598..50bc0b8b2b26e1496779686c3f39f87b57e27ff7 100644
--- a/theories/typing/lib/vec/vec_index.v
+++ b/theories/typing/lib/vec/vec_index.v
@@ -25,7 +25,7 @@ Section vec_index.
     rewrite !tctx_hasty_val.
     iDestruct "v" as ([|d]) "[⧖ v]"=>//. case v as [[|v|]|]=>//=.
     iDestruct "i" as ([|]) "[_ i]"=>//. case i as [[|i|]|]=>//=.
-    wp_bind (new _). iApply wp_new; [done..|]. iIntros "!>% [†r ↦r]".
+    wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]".
     iDestruct "v" as "[(%vl & ↦v & vec) †v]". move: d=> [|d]//=.
     case vl as [|[[]|][]]=>//=. move: d=> [|d]//=.
     iDestruct "vec" as (??? aπl ->) "[Bor tys]".
@@ -36,9 +36,8 @@ Section vec_index.
     iDestruct "↦" as "(↦₀ & ↦₁ & ↦₂ &_)". wp_let. do 3 wp_read. do 2 wp_op. wp_write.
     iMod ("Toα" with "[$↦₀ $↦₁ $↦₂]") as "α". iMod ("ToL" with "α L") as "L".
     do 2 rewrite -heap_mapsto_vec_singleton freeable_sz_full.
-    wp_bind (delete _). iApply (wp_delete with "[$↦v $†v]"); [done|].
-    iIntros "!> _". wp_seq. wp_bind (delete _).
-    iApply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "!> _". do 3 wp_seq.
+    wp_apply (wp_delete with "[$↦v $†v]"); [done|]. iIntros "_". wp_seq.
+    wp_apply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "_". do 3 wp_seq.
     iMod (proph_obs_sat with "PROPH Obs") as %(?& inat &?&->& Lkup &_); [done|].
     move: Lkup. rewrite -vec_to_list_apply -vlookup_lookup'. move=> [In _].
     set ifin := nat_to_fin In. have Eqi: inat = ifin by rewrite fin_to_nat_to_fin.
@@ -64,7 +63,7 @@ Section vec_index.
     rewrite !tctx_hasty_val.
     iDestruct "v" as ([|d]) "[#⧖ v]"=>//. case v as [[|v|]|]=>//=.
     iDestruct "i" as ([|]) "[_ i]"=>//. case i as [[|i|]|]=>//=.
-    wp_bind (new _). iApply wp_new; [done..|]. iIntros "!>% [†r ↦r]".
+    wp_apply wp_new; [done..|]. iIntros (?) "[†r ↦r]".
     iDestruct "v" as "[(%vl & ↦v & #In & uniq) †v]". case vl as [|[[]|][]]=>//=.
     iDestruct "i" as "[(%& ↦i & (%&->&->)) †i]". rewrite !heap_mapsto_vec_singleton.
     iDestruct "uniq" as (d' ξi [Le Eq2]) "[Vo Bor]". set ξ := PrVar _ ξi.
@@ -78,8 +77,8 @@ Section vec_index.
     have ->: vπ = λ π, (lapply aπl π: list _, π ξ).
     { rewrite [vπ]surjective_pairing_fun. by rewrite Eq1 Eq2. }
     do 3 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|]. iIntros "!>_". wp_seq.
+    rewrite !freeable_sz_full.
+    wp_apply (wp_delete with "[$↦v $†v]"); [done|]. iIntros "_". wp_seq.
     wp_bind (delete _). iApply (wp_cumulative_time_receipt with "TIME"); [done|].
     iApply (wp_delete with "[$↦i $†i]"); [done|]. iIntros "!>_ ⧗". wp_seq.
     iMod (proph_obs_sat with "PROPH Obs") as %(?& Obs); [done|].
diff --git a/theories/typing/lib/vec/vec_pushpop.v b/theories/typing/lib/vec/vec_pushpop.v
index eedf1b111779b7d65301db1682fe98174be6209c..2e0336f53da3bbc0308443216a5be47f8b258af6 100644
--- a/theories/typing/lib/vec/vec_pushpop.v
+++ b/theories/typing/lib/vec/vec_pushpop.v
@@ -37,11 +37,11 @@ Section vec_pushpop.
     wp_bind (delete _). rewrite -heap_mapsto_vec_singleton freeable_sz_full.
     iApply (wp_persistent_time_receipt with "TIME ⧖x"); [done|].
     iApply (wp_delete with "[$↦v $†v]"); [done|]. iIntros "!>_ ⧖x".
-    iCombine "⧖u ⧖x" as "#⧖". wp_seq. wp_bind (vec_push_core _ _).
-    iApply (wp_vec_push_core with "[↦l ↦tys ↦ex † ↦ty]"). { iExists _, _. iFrame. }
-    iIntros "!>(%&%& ↦ & ↦tys & ↦ex & † & (%& %Len & ↦x))". wp_seq.
-    rewrite freeable_sz_full. wp_bind (delete _).
-    iApply (wp_delete with "[$↦x †x]"); [lia|by rewrite Len|]. iIntros "!>_".
+    iCombine "⧖u ⧖x" as "#⧖". wp_seq.
+    wp_apply (wp_vec_push_core with "[↦l ↦tys ↦ex † ↦ty]"). { iExists _, _. iFrame. }
+    iIntros "(%&%& ↦ & ↦tys & ↦ex & † & (%& %Len & ↦x))". wp_seq.
+    rewrite freeable_sz_full.
+    wp_apply (wp_delete with "[$↦x †x]"); [lia|by rewrite Len|]. iIntros "_".
     wp_seq. set vπ' := λ π, (lapply (vsnoc aπl bπ) π, π ξ).
     iMod (uniq_update with "UNIQ Vo Pc") as "[Vo Pc]"; [done|].
     iMod ("ToBor" with "[↦ ↦tys ↦ex † Pc]") as "[Bor α]".
@@ -112,7 +112,7 @@ Section vec_pushpop.
     iDestruct (big_sepL_vinitlast with "↦tys") as "[↦tys (%vl & ↦last & ty)]"=>/=.
     set vπ' := λ π, (lapply (vinit aπl) π, π ξ).
     wp_op. wp_let. wp_op. wp_write. do 2 wp_op. wp_read. wp_op. wp_write.
-    wp_bind (new _). iApply wp_new; [lia|done|]. iIntros "!>" (r) "[†r ↦r]". wp_let.
+    wp_apply wp_new; [lia|done|]. iIntros (r) "[†r ↦r]". wp_let.
     rewrite Nat2Z.id /= heap_mapsto_vec_cons. have ->: (S len - 1)%Z = len by lia.
     iDestruct "↦r" as "[↦r ↦r']". iDestruct (ty_size_eq with "ty") as %Eqvl.
     wp_write. wp_op. wp_read. do 2 wp_op. rewrite -Nat2Z.inj_mul.
diff --git a/theories/typing/lib/vec_util.v b/theories/typing/lib/vec_util.v
index 47eaf416741d5a99bc30ed6978c2e4909512002d..47e25983a96f96e0e955ca5bafe0338b4ca59b7f 100644
--- a/theories/typing/lib/vec_util.v
+++ b/theories/typing/lib/vec_util.v
@@ -62,15 +62,15 @@ Section vec_util.
         iStopProof. do 3 f_equiv. apply ty_own_depth_mono. lia.
       - rewrite big_sepL_singleton. iExists _. rewrite Nat.add_0_r vec_to_list_length.
         iFrame "↦new". iApply ty_own_depth_mono; [|done]. lia. }
-    rewrite plus_0_r. wp_op. wp_write. do 3 wp_op. wp_bind (new _).
-    iApply wp_new; [lia|done|]. iIntros "!> % [†' ↦l']". wp_let.
+    rewrite plus_0_r. wp_op. wp_write. do 3 wp_op.
+    wp_apply wp_new; [lia|done|]. iIntros (?) "[†' ↦l']". wp_let.
     have ->: ∀sz: nat, ((2 * len + 1) * sz)%Z = len * sz + (sz + len * sz) by lia.
     rewrite Nat2Z.id !repeat_app !heap_mapsto_vec_app !repeat_length shift_loc_assoc_nat.
     iDestruct "↦l'" as "(↦l' & ↦new & ↦ex')".
-    iDestruct (big_sepL_ty_own_length with "tys") as %Lwll. wp_op. wp_bind (memcpy _).
-    iApply (wp_memcpy with "[$↦l' $↦l]"); [rewrite repeat_length; lia|lia|].
-    iIntros "!>[↦l' ↦l]". wp_seq. wp_op. rewrite -Nat2Z.inj_mul. wp_bind (delete _).
-    iApply (wp_delete with "[$↦l †]"); [lia|by rewrite Lwll|]. iIntros "!>_".
+    iDestruct (big_sepL_ty_own_length with "tys") as %Lwll. wp_op.
+    wp_apply (wp_memcpy with "[$↦l' $↦l]"); [rewrite repeat_length; lia|lia|].
+    iIntros "[↦l' ↦l]". wp_seq. wp_op. rewrite -Nat2Z.inj_mul.
+    wp_apply (wp_delete with "[$↦l †]"); [lia|by rewrite Lwll|]. iIntros "_".
     wp_seq. wp_write. do 2 wp_op. rewrite -Nat2Z.inj_mul.
     iApply (wp_memcpy with "[$↦new $↦x]"); [by rewrite repeat_length|lia|].
     iIntros "!> [↦new ↦x]". iApply "ToΦ". iExists _, _.