Fix 822--823.

1 files changed, 3 insertions, 1 deletions

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index 732154f..77b5ce7 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -120,7 +120,9 @@ let step (t : Term) : Term =
   \caption{Implementation of complete development.}\label{lst:step}
 \end{listing}
 
-\TODO{explain why fuel is necessary for the reducer}
+Our reducer only applies \(\beta\)-reduction. It is also possible to
+perform \(\eta\)-contraction as computing a strengthened term requires only
+structural induction.
 
 \subsection{Encoding Algorithm}%
 \label{subsec:encoding}