From 59314ba5a147195f36b138f0fccb06079de0543b Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 17:44:44 +0100
Subject: Fix 822--823.

---
 sec/reducer.ltx | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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}
-- 
cgit v1.2.3