diff --git a/theories/examples/list_sort_elem_client.v b/theories/examples/list_sort_elem_client.v
index 7d1557b6a11828a24d892e4e21dfbd82d29863ac..9999135183bc8cae17bfdab84a4b0ec39bc8804c 100644
--- a/theories/examples/list_sort_elem_client.v
+++ b/theories/examples/list_sort_elem_client.v
@@ -42,23 +42,23 @@ Section list_sort_elem_client.
     by rewrite -assoc_L.
   Qed.
 
-  Lemma recv_all_spec c p xs ys :
-    Sorted R ys →
-    {{{ c ↣ tail_protocol I R xs ys <++> p @ N }}}
+  Lemma recv_all_spec c p xs ys' :
+    Sorted R ys' →
+    {{{ c ↣ tail_protocol I R xs ys' <++> p @ N }}}
       recv_all c
-    {{{ ys' ws, RET (val_encode ws);
-        ⌜Sorted R (ys ++ ys')⌝ ∗ ⌜ys ++ ys' ≡ₚ xs⌝ ∗
-        c ↣ p @ N ∗ [∗ list] y;w ∈ ys';ws, I y w
+    {{{ ys ws, RET (val_encode ws);
+        ⌜Sorted R (ys' ++ ys)⌝ ∗ ⌜ys' ++ ys ≡ₚ xs⌝ ∗
+        c ↣ p @ N ∗ [∗ list] y;w ∈ ys;ws, I y w
     }}}.
   Proof.
     iIntros (Hsort Φ) "Hc HΦ".
-    iLöb as "IH" forall (xs ys Φ Hsort).
+    iLöb as "IH" forall (xs ys' Φ Hsort).
     wp_lam. wp_branch as "_" "Hperm"; wp_pures.
     - wp_recv (y v) as (Htl) "HIxv".
       wp_apply ("IH" with "[] Hc"); first by auto using Sorted_snoc.
-      iIntros (ys' ws). rewrite -!assoc_L. iDestruct 1 as (??) "[Hc HI]".
+      iIntros (ys ws). rewrite -!assoc_L. iDestruct 1 as (??) "[Hc HI]".
       wp_apply (lcons_spec (A:=val) with "[//]"); iIntros (_).
-      iApply ("HΦ" $! (y :: ys')). simpl; iFrame; auto.
+      iApply ("HΦ" $! (y :: ys)). simpl; iFrame; auto.
     - wp_apply (lnil_spec with "[//]"); iIntros (_).
       iApply ("HΦ" $! [] []); rewrite /= right_id_L; by iFrame.
   Qed.