diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 825924714786ae06f12db190054969c4605ca774..406ec94a3800c336485ba6122965b75e6e04ccc2 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -4,20 +4,14 @@ From iris.heap_lang Require Import proofmode notation.
 From osiris.utils Require Import list.
 
 Definition lmerge : val :=
-  rec: "go" "cmp" "hys" "hzs" :=
-    match: "hys" with
-      NONE => "hzs"
-    | SOME "_" =>
-      match: "hzs" with
-        NONE => "hys"
-      | SOME "_" =>
-        let: "y" := lhead "hys" in
-        let: "z" := lhead "hzs" in
-        if: "cmp" "y" "z"
-        then lcons "y" ("go" "cmp" (ltail "hys") "hzs")
-        else lcons "z" ("go" "cmp" "hys" (ltail "hzs"))
-      end
-    end.
+  rec: "go" "cmp" "ys" "zs" :=
+    if: lisnil "ys" then "zs" else
+    if: lisnil "zs" then "ys" else
+    let: "y" := lhead "ys" in
+    let: "z" := lhead "zs" in
+    if: "cmp" "y" "z"
+    then lcons "y" ("go" "cmp" (ltail "ys") "zs")
+    else lcons "z" ("go" "cmp" "ys" (ltail "zs")).
 
 Definition list_sort_service : val :=
   rec: "go" "c" :=
@@ -70,12 +64,12 @@ Section list_sort.
     {{{ ws, RET val_encode ws; [∗ list] x;v ∈ list_merge R xs1 xs2;ws, I x v }}}.
   Proof.
     iIntros "#Hcmp" (Ψ) "!> [HI1 HI2] HΨ". iLöb as "IH" forall (xs1 xs2 vs1 vs2 Ψ).
-    destruct xs1 as [|x1 xs1], vs1 as [|v1 vs1]; simpl; try done.
-    { wp_lam. wp_pures. iApply "HΨ". by rewrite list_merge_nil_l. }
-    wp_lam; wp_pures.
-    destruct xs2 as [|x2 xs2], vs2 as [|v2 vs2]; simpl; try done.
-    { wp_pures. iApply "HΨ". iFrame. }
-    wp_pures.
+    wp_lam. wp_apply (lisnil_spec (A:=val) with "[//]"); iIntros (_).
+    destruct xs1 as [|x1 xs1], vs1 as [|v1 vs1]; simpl; done || wp_pures.
+    { iApply "HΨ". by rewrite list_merge_nil_l. }
+    wp_apply (lisnil_spec (A:=val) with "[//]"); iIntros (_).
+    destruct xs2 as [|x2 xs2], vs2 as [|v2 vs2]; simpl; done || wp_pures.
+    { iApply "HΨ". iFrame. }
     wp_apply (lhead_spec (A:=val) with "[//]"); iIntros (_).
     wp_apply (lhead_spec (A:=val) with "[//]"); iIntros (_).
     iDestruct "HI1" as "[HI1 HI1']"; iDestruct "HI2" as "[HI2 HI2']".
diff --git a/theories/utils/list.v b/theories/utils/list.v
index 58fe05e39ed3098eb0dfd556543478d963f17a12..4d0702ef9976a7fcb4de38940876a34209c6ede8 100644
--- a/theories/utils/list.v
+++ b/theories/utils/list.v
@@ -14,6 +14,12 @@ Instance list_val_enc `{ValEnc A} : ValEnc (list A) :=
 Definition lnil : val := λ: <>, NONEV.
 Definition lcons : val := λ: "x" "l", SOME ("x", "l").
 
+Definition lisnil : val := λ: "l",
+  match: "l" with
+    SOME "p" => #false
+  | NONE => #true
+  end.
+
 Definition lhead : val := λ: "l",
   match: "l" with
     SOME "p" => Fst "p"
@@ -106,6 +112,12 @@ Lemma lcons_spec x xs :
   {{{ RET val_encode (x :: xs); True }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
 
+Lemma lisnil_spec xs:
+  {{{ True }}}
+    lisnil (val_encode xs)
+  {{{ RET #(if xs is [] then true else false); True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. destruct xs; wp_pures; by iApply "HΦ". Qed.
+
 Lemma lhead_spec x xs:
   {{{ True }}} lhead (val_encode (x::xs)) {{{ RET val_encode x; True }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.