diff --git a/theories/encodings/list.v b/theories/encodings/list.v
index c0ccf3e394f2478e858abca83889bf6130260c16..aca68f34bcb4998907693366a2dbfd020b4e1b8d 100644
--- a/theories/encodings/list.v
+++ b/theories/encodings/list.v
@@ -66,6 +66,13 @@ Definition lsnoc : val :=
     | NONE => lcons "x" NONE
     end.
 
+Definition lsplit : val :=
+  λ: "xs",
+  let: "hd" := lhead "xs" in
+  let: "ys" := lcons "hd" NONEV in
+  let: "zs" := ltail "xs" in
+  ("ys", "zs").
+
 Section lists.
 Context `{heapG Σ}.
 Implicit Types i : nat.
@@ -175,4 +182,18 @@ Proof.
   iIntros (_). by wp_apply lcons_spec=> //.
 Qed.
 
+Lemma lsplit_spec xs x :
+  {{{ True }}} lsplit (encode (x::xs)) {{{ RET (encode [x],encode xs); True }}}.
+Proof.
+  iIntros (Φ _) "HΦ". 
+  wp_lam. wp_apply (lhead_spec)=> //.
+  iIntros (_).
+  wp_apply (lcons_spec _ [])=> //.
+  iIntros (_).
+  wp_apply (ltail_spec)=> //.
+  iIntros (_).
+  wp_pures.
+  by iApply "HΦ".
+Qed.
+
 End lists.
\ No newline at end of file
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 9706add78d30af6625e2dd5854d63031c1f1eaf0..555e874bc47e10352db031a52a8612f5fe16df02 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -11,29 +11,6 @@ Require Import Omega.
 Section ListSortExample.
   Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).
 
-  Definition lsplit : val :=
-    λ: "xs",
-      let: "hd" := lhead "xs" in
-      let: "ys" := lcons "hd" NONEV in
-      let: "zs" := ltail "xs" in
-    ("ys", "zs").
-
-  Lemma lsplit_spec (x : Z) (xs : list Z) :
-    {{{ True }}}
-      lsplit (encode (x::xs))
-    {{{ RET (encode [x],encode xs); True }}}.
-  Proof.
-    iIntros (Φ _) "HΦ".
-    wp_lam. wp_apply (lhead_spec (T := Z))=> //.
-    iIntros (_).
-    wp_apply (lcons_spec (T := Z) _ [])=> //.
-    iIntros (_).
-    wp_apply (ltail_spec (T := Z))=> //.
-    iIntros (_).
-    wp_pures.
-    by iApply "HΦ".
-  Qed.
-
   Definition lsplit_ref : val :=
     λ: "xs", let: "ys_zs" := lsplit !"xs" in
              (ref (Fst "ys_zs"), ref (Snd ("ys_zs"))).
@@ -48,7 +25,7 @@ Section ListSortExample.
         lzs ↦ encode zs }}}.
   Proof.
     iIntros (Φ) "Hhd HΦ".
-    wp_lam. wp_load. wp_apply (lsplit_spec)=> //; iIntros (_).
+    wp_lam. wp_load. wp_apply (lsplit_spec (T:=Z))=> //; iIntros (_).
     wp_alloc lzs as "Hlzs".
     wp_alloc lys as "Hlys".
     wp_pures.