Fix 126--131.

1 files changed, 7 insertions, 5 deletions

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}