Fix 825--830.

1 files changed, 9 insertions, 6 deletions

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