diff --git a/src/goose_lang/lib/slice/slice.v b/src/goose_lang/lib/slice/slice.v
index effe081cc..455fd2c02 100644
--- a/src/goose_lang/lib/slice/slice.v
+++ b/src/goose_lang/lib/slice/slice.v
@@ -739,6 +739,40 @@ Proof.
   word.
 Qed.
 
+Lemma own_slice_cap_take s t n vs :
+  uint.Z n ≤ uint.Z s.(Slice.sz) →
+  own_slice_small (slice_skip s t n) t (DfracOwn 1) (drop (uint.nat n) vs) ∗
+    own_slice_cap s t -∗
+  own_slice_cap (slice_take s n) t.
+Proof.
+  iIntros (Hn) "[Hskip Hcap]".
+  iDestruct (own_slice_cap_wf with "Hcap") as %Hwf.
+  rewrite /own_slice_cap /own_slice_small.
+  iDestruct "Hskip" as "[Hskip [%Hvs_len %Hskip_wf]]".
+  simpl in Hvs_len, Hskip_wf.
+  rewrite -> !word.unsigned_sub_nowrap in * by word.
+  rewrite length_drop in Hvs_len.
+  iDestruct "Hcap" as (extra Hextra_len) "Hcap".
+  iExists (drop (uint.nat n) vs ++ extra).
+  iSplit.
+  { iPureIntro.
+    simpl.
+    rewrite length_app length_drop.
+    word. }
+  simpl.
+  rewrite array_app.
+  iFrame "Hskip".
+
+  iExactEq "Hcap".
+  rewrite length_drop.
+  rewrite loc_add_assoc.
+  f_equal.
+  f_equal.
+  rewrite -Z.mul_add_distr_l.
+  f_equal.
+  word.
+Qed.
+
 (** We have full ownership, and take into the capacity.
 Cannot be typed, since [extra] might not be valid at this type. *)
 Lemma wp_SliceTake_full_cap {stk E s} t vs (n: u64):
diff --git a/src/goose_lang/lib/slice/typed_slice.v b/src/goose_lang/lib/slice/typed_slice.v
index 5ded35d43..dd6b6b041 100644
--- a/src/goose_lang/lib/slice/typed_slice.v
+++ b/src/goose_lang/lib/slice/typed_slice.v
@@ -264,6 +264,88 @@ Proof.
   iApply ("HΦ" with "[$]").
 Qed.
 
+Lemma wp_SliceTake_small {stk E s} t q vs (n: u64):
+  uint.Z n ≤ length vs →
+  {{{ own_slice_small s t q vs }}}
+    SliceTake (slice_val s) #n @ stk; E
+  {{{ RET (slice_val (slice_take s n)); own_slice_small (slice_take s n) t q (take (uint.nat n) vs) }}}.
+Proof.
+  iIntros (Hbound Φ) "Hs HΦ".
+  rewrite /own_slice_small.
+  wp_apply (slice.wp_SliceTake_small with "[$Hs]").
+  { rewrite list_untype_length //. }
+  rewrite /list.untype fmap_take //.
+Qed.
+
+Lemma wp_SliceSkip_small s t q vs (n : u64) :
+  uint.Z n ≤ length vs →
+  {{{ own_slice_small s t q vs }}}
+    SliceSkip t (slice_val s) #n
+  {{{ s', RET (slice_val s'); own_slice_small s' t q (drop (uint.nat n) vs) }}}.
+Proof.
+  iIntros (Hbound Φ) "Hs HΦ".
+  rewrite /own_slice_small. rewrite /list.untype fmap_drop.
+  wp_apply (slice.wp_SliceSkip_small with "[$Hs]").
+  { rewrite length_fmap; auto. }
+  auto.
+Qed.
+
+Lemma wp_SliceSkip_full s t q vs (n : u64) :
+  uint.Z n ≤ length vs →
+  {{{ own_slice s t q vs }}}
+    SliceSkip t (slice_val s) #n
+  {{{ s', RET (slice_val s'); own_slice s' t q (drop (uint.nat n) vs) }}}.
+Proof.
+  iIntros (Hbound Φ) "Hs HΦ".
+  iDestruct (own_slice_sz with "Hs") as %Hsz.
+  wp_apply slice.wp_SliceSkip.
+  { word. }
+  iApply "HΦ".
+  iApply own_slice_split.
+  iDestruct (own_slice_split_1 with "Hs") as "[Hs Hcap]".
+  rewrite /own_slice_small. rewrite /list.untype fmap_drop.
+  iDestruct (slice.slice_small_split with "Hs") as "[Hs1 $]".
+  { rewrite length_fmap; word. }
+  iApply (own_slice_cap_skip with "[$Hcap]").
+  { word. }
+Qed.
+
+(* construct the capacity of a slice_take expression from ownership over the
+rest of the slice (expressed using [slice_skip]) and the original capacity. *)
+Lemma own_slice_cap_take s t n vs :
+  uint.Z n ≤ uint.Z s.(Slice.sz) →
+  own_slice_small (slice_skip s t n) t (DfracOwn 1) (drop (uint.nat n) vs) ∗
+    own_slice_cap s t -∗
+  own_slice_cap (slice_take s n) t.
+Proof.
+  iIntros (Hn) "[Hskip Hcap]".
+  rewrite /own_slice_small.
+  iApply (slice.own_slice_cap_take with "[Hskip $Hcap]").
+  { auto. }
+  rewrite /list.untype fmap_drop. iFrame.
+Qed.
+
+(* Take a prefix s[:n] while retaining the capacity, which now includes the
+elements from n to the original length. Since the capacity must be fully owned,
+this variant requires full ownership of the slice and not a partial fraction. *)
+Lemma wp_SliceTake_full {stk E s} t vs (n: u64):
+  uint.Z n ≤ length vs →
+  {{{ own_slice s t (DfracOwn 1) vs }}}
+    SliceTake (slice_val s) #n @ stk; E
+  {{{ RET (slice_val (slice_take s n)); own_slice (slice_take s n) t (DfracOwn 1) (take (uint.nat n) vs) }}}.
+Proof.
+  iIntros (Hbound Φ) "Hs HΦ".
+  iDestruct (own_slice_sz with "Hs") as %Hsz.
+  iDestruct (own_slice_split_1 with "Hs") as "[Hs Hcap]".
+  iDestruct (own_slice_cap_wf with "Hcap") as %Hcap.
+  wp_apply (slice.wp_SliceTake).
+  { word. }
+  iApply "HΦ".
+  iDestruct (slice_small_split with "Hs") as "[$ Hdrop]".
+  { word. }
+  iApply own_slice_cap_take; [ word | ]. iFrame.
+Qed.
+
 Lemma wp_SliceSet stk E s t `{!IntoValForType V t} vs (i: u64) v :
   {{{ own_slice_small s t (DfracOwn 1) vs ∗ ⌜ is_Some (vs !! uint.nat i) ⌝ }}}
     SliceSet t (slice_val s) #i (to_val v) @ stk; E
@@ -487,12 +569,13 @@ Proof.
   word.
 Qed.
 
-Lemma wp_SliceCopy_full_typed stk E sl t q vs dst vs' :
+Lemma wp_SliceCopy_full stk E sl t q vs dst vs' :
   {{{ own_slice_small sl t q vs ∗ own_slice_small dst t (DfracOwn 1) vs' ∗ ⌜length vs = length vs'⌝}}}
     SliceCopy t (slice_val dst) (slice_val sl) @ stk; E
-  {{{ RET #(W64 (length vs)); own_slice_small sl t q vs ∗ own_slice_small dst t (DfracOwn 1) vs }}}.
+  {{{ (l: w64), RET #l; ⌜uint.nat l = length vs⌝ ∗ own_slice_small sl t q vs ∗ own_slice_small dst t (DfracOwn 1) vs }}}.
 Proof.
   iIntros (Φ) "(Hsrc & Hdst & %Hlen) HΦ".
+  iDestruct (own_slice_small_sz with "Hsrc") as %Hsz.
   wp_apply (wp_SliceCopy with "[$Hsrc $Hdst]"); [word|].
   iIntros "(? & ?)".
   rewrite Hlen.
@@ -500,6 +583,8 @@ Proof.
   list_simplifier.
   iApply "HΦ".
   iFrame.
+  iPureIntro.
+  word.
 Qed.
 
 Lemma wp_SliceCopy_subslice stk E sl (n1 n2: u64) t q vs dst vs' :
diff --git a/src/program_proof/marshal_stateless_proof.v b/src/program_proof/marshal_stateless_proof.v
index 4c7d3c440..9da3a57cc 100644
--- a/src/program_proof/marshal_stateless_proof.v
+++ b/src/program_proof/marshal_stateless_proof.v
@@ -21,7 +21,7 @@ Proof.
   { rewrite /list.untype fmap_app take_app_length' //. }
   iIntros "Hs".
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite /list.untype length_fmap length_app /=. word. }
+  { len. }
   iIntros (s') "Hs'". wp_pures. iApply "HΦ". done.
 Qed.
 
@@ -35,7 +35,7 @@ Proof.
   { rewrite /list.untype fmap_app take_app_length' //. }
   iIntros "Hs".
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite /list.untype length_fmap length_app /=. word. }
+  { len. }
   iIntros (s') "Hs'". wp_pures. iApply "HΦ". done.
 Qed.
 
@@ -49,13 +49,15 @@ Proof.
   iMod (own_slice_small_persist with "Hs") as "#Hs".
   wp_rec. wp_pures.
   wp_apply (wp_SliceTake_small with "Hs").
-  { rewrite /list.untype fmap_app length_app !length_fmap. word. }
+  { len. }
   iIntros "Hs1".
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite /list.untype length_fmap length_app /=. word. }
+  { len. }
   iIntros (s') "Hs2". wp_pures. iApply "HΦ".
-  { rewrite /list.untype -fmap_take -fmap_drop.
-    rewrite take_app_length' // drop_app_length' //. iFrame. done. }
+  iModIntro.
+  rewrite take_app_length' //.
+  rewrite drop_app_length' //.
+  iFrame.
 Qed.
 
 Theorem wp_ReadBytesCopy s q (len: u64) (head tail : list u8) :
@@ -75,17 +77,17 @@ Proof.
   { rewrite length_app. word. }
   iDestruct (own_slice_small_acc with "Hb") as "[Hb Hbclose]".
   wp_apply (wp_SliceCopy_full with "[$Hs $Hb]").
-  { iPureIntro. rewrite !list_untype_length length_replicate length_take length_app. word. }
-  iIntros "[Hs Hb]".
+  { iPureIntro. len. }
+  iIntros (l) "(%Hl_val & Hs & Hb)".
   iDestruct (own_slice_combine with "Hs Hsclose") as "Hs".
   { word. }
   rewrite take_drop.
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite list_untype_length length_app. word. }
+  { len. }
   iIntros (s') "Hs'".
   wp_pures. iApply "HΦ". iModIntro. iSplitR "Hs'".
   - iApply "Hbclose". rewrite take_app_length' //.
-  - rewrite /list.untype -fmap_drop drop_app_length' //.
+  - rewrite drop_app_length' //.
 Qed.
 
 Theorem wp_ReadBool s q (bit: u8) (tail: list u8) :
@@ -99,9 +101,8 @@ Proof.
   wp_apply (wp_SliceGet with "[$Hs]"); [ auto | ].
   iIntros "Hs".
   wp_pures.
-  (* TODO: this wp seems to come from untyped library *)
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite list_untype_length /=. word. }
+  { len. }
   iIntros (s') "Hs".
   wp_pures. iModIntro.
   iApply "HΦ".
@@ -112,9 +113,7 @@ Proof.
       split.
     - inversion 1; subst; auto.
     - intros H.
-      do 2 f_equal.
-      apply (inj uint.Z). (* don't know how I even figured this out *)
-      change (uint.Z (U8 0)) with 0%Z; assumption.
+      repeat (f_equal; try word).
     }
     destruct (decide _), (decide _); auto; tauto.
   }
@@ -157,7 +156,7 @@ Proof.
     iIntros (ptr) "Hnew". wp_pures.
     iDestruct (slice.own_slice_to_small with "Hs") as "Hs".
     iDestruct (slice.own_slice_small_acc with "Hnew") as "[Hnew Hcl]".
-    wp_apply (wp_SliceCopy_full with "[Hnew Hs]").
+    wp_apply (slice.wp_SliceCopy_full with "[Hnew Hs]").
     { iFrame. iPureIntro. rewrite list_untype_length Hsz length_replicate //. }
     iIntros "[_ Hnew]". iDestruct ("Hcl" with "Hnew") as "Hnew".
     wp_pures. iApply "HΦ". iModIntro. iFrame. iPureIntro. simpl. word.
@@ -243,17 +242,8 @@ Theorem wp_WriteBool s (vs: list u8) (b: bool) :
 Proof.
   iIntros (Φ) "Hs HΦ". wp_rec. wp_pures.
   destruct b; wp_pures.
-  (* TODO: this also breaks through the typed slice library *)
-  - wp_apply (wp_SliceAppend' with "Hs"); auto.
-    iIntros (s') "Hs".
-    iApply "HΦ".
-    rewrite /own_slice.
-    rewrite list_untype_app //.
-  - wp_apply (wp_SliceAppend' with "Hs"); auto.
-    iIntros (s') "Hs".
-    iApply "HΦ".
-    rewrite /own_slice.
-    rewrite list_untype_app //.
+  - wp_apply (wp_SliceAppend with "Hs"); auto.
+  - wp_apply (wp_SliceAppend with "Hs"); auto.
 Qed.
 
 End goose_lang.
diff --git a/src/program_proof/std_proof.v b/src/program_proof/std_proof.v
index 8826653d2..991ef4a01 100644
--- a/src/program_proof/std_proof.v
+++ b/src/program_proof/std_proof.v
@@ -190,6 +190,24 @@ Proof.
   word.
 Qed.
 
+Lemma wp_SliceSplit_full s dq (xs: list w8) (n: w64) :
+  {{{ own_slice s byteT dq xs ∗ ⌜uint.Z n < Z.of_nat (length xs)⌝ }}}
+    SliceSplit (to_val s) #n
+  {{{ RET (to_val (slice_take s n), to_val (slice_skip s byteT n));
+      own_slice_small (slice_take s n) byteT dq (take (uint.nat n) xs) ∗
+      own_slice (slice_skip s byteT n) byteT dq (drop (uint.nat n) xs)
+  }}}.
+Proof.
+  iIntros (Φ) "[Hs %Hn] HΦ".
+  iDestruct (own_slice_sz with "Hs") as %Hsz.
+  iDestruct (own_slice_split_1 with "Hs") as "[Hs Hcap]".
+  wp_apply (wp_SliceSplit with "[$Hs]"); [ done | ].
+  iIntros "[Htake Hskip]".
+  iApply "HΦ". iFrame "Htake".
+  iApply own_slice_split; iFrame "Hskip".
+  iApply (own_slice_cap_skip with "Hcap"). word.
+Qed.
+
 Lemma wp_SumNoOverflow (x y : u64) stk E :
   ∀ Φ : val → iProp Σ,
     Φ #(bool_decide (uint.Z (word.add x y) = (uint.Z x + uint.Z y)%Z)) -∗