diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md
index 1f0020d1..56cd7816 100644
--- a/src/plfa/part1/Lists.lagda.md
+++ b/src/plfa/part1/Lists.lagda.md
@@ -1089,12 +1089,13 @@ into two lists that merge to give the original list, where all
 elements of one list satisfy the predicate, and all elements of
 the other do not satisfy the predicate.
 
-Define the following variant of the traditional `filter` function on lists,
-which given a decidable predicate and a list returns all elements of the
-list satisfying the predicate:
+Define the following variant of the traditional `filter` function on
+lists, which given a decidable predicate and a list returns a list of
+elements that satisfy the predicate and a list of elements that don't,
+with their corresponding proofs.
 
-    split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (xs : List A)
-      → ∃[ ys ] ∃[ zs ] ( merge xs ys zs × All P ys × All (¬_ ∘ P) zs )
+    split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A)
+      → ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )
 
 ```
 -- Your code goes here