diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md
index 0f329662..8609ce79 100644
--- a/src/plfa/part1/Lists.lagda.md
+++ b/src/plfa/part1/Lists.lagda.md
@@ -1076,9 +1076,10 @@ 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) (zs : List A)
       → ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )