From dac18624162e82fb59b1432d94dbf33e734026a7 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 18:09:53 +0100
Subject: Fix 126--131.

---
 sec/systemt.ltx | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index cfcd660..57a0bdf 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -92,11 +92,13 @@ encode a data type, there are three operations we need to account for:
 As a concrete example, consider the pseudocode in \cref{lst:tree-eq}
 for comparing whether two binary trees are equal. We use a fold to
 create an equality predicate out of \systemtinline{tree1}. When
-\systemtinline{tree1} is a leaf, we pattern match on the other tree to
-see if it is also a leaf. If \systemtinline{tree1} is instead a
-branch, we obtain equality predicates for its two subtrees by the
-induction principal. We again pattern match on the other tree and test
-equality recursively when it is also a branch.
+\systemtinline{tree1} is a leaf, we pattern match on the other tree
+\systemtinline{t} to see if it is also a leaf. If
+\systemtinline{tree1} is instead a branch, the \foldkw{} provides
+equality predicates \systemtinline{l} and \systemtinline{r} for its
+two subtrees by the induction principal. We again pattern match on the
+other tree and when it is also a branch we test equality recursively
+with the predicates.
 
 \begin{listing}
   \begin{systemt}
-- 
cgit v1.2.3

