From 860938c1a4c912029c1ff9535805ff20ff7aa05b Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 17:41:46 +0100
Subject: Fix 815--522.

---
 sec/reducer.ltx | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'sec/reducer.ltx')

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index 1e5757b..732154f 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -75,7 +75,7 @@ let rename (t : Term) : (Nat -> Nat) -> Term =
 
 The main driver in the reducer is the \verb|step| function, which
 performs a complete development of a term. We give its definition in
-\cref{lst:step}. By induction, all terms within the \verb|foldcase|
+\cref{lst:step}. By induction, all terms within the induction hypothesis
 have been completely developed. Most cases pass through their
 arguments unchanged: the only reductions for \(\suc~t\) happen within
 \(t\) for instance. The two interesting cases are \verb|Primrec| and
-- 
cgit v1.2.3

