From d783dd8c54f71d11d12b676d2f22ca1e7d7a3028 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 17:48:27 +0100
Subject: Fix 825--830.

---
 sec/reducer.ltx | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'sec/reducer.ltx')

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index 77b5ce7..2079e49 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -127,13 +127,16 @@ structural induction.
 \subsection{Encoding Algorithm}%
 \label{subsec:encoding}
 
-In \cref{M-sec:encoding} we described a process to embed \lang{}
+In \cref{M-sec:encoding} we described an algorithm to embed \lang{}
 within System~T. We have written this algorithm in \lang{} itself,
-simultaneously mechanising the conversion and proving it is
-terminating. Our input is type-annotated \lang{} terms, and we output
-unannotated System~T terms as in \cref{lst:term-ty}. Each phase is
-accompanied by its own inductive types representing types and
-type-annotated terms.
+simultaneously mechanising the conversion and indirectly proving it is
+terminating. Our input is a type-annotated \lang{} term, and we output
+an unannotated System~T term as in \cref{lst:term-ty}. Each phase is
+accompanied by its own inductive types representing the phases' types
+and terms. To compute the encoding, any term formers that are not in
+System~T must be annotated with their types. For simplicity, our
+finite sums and products are over unlabelled lists of types instead of
+finite sets.
 
 Folds in \lang{} are destructive---the inductive components used to
 generate the induction hypothesis are unnamed. This has some
-- 
cgit v1.2.3

