From 66450ee5c829e7c00ffa3fca786b4e65bc7c5733 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 17:57:10 +0100
Subject: Fix 31--37.

---
 sec/intro.ltx | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'sec/intro.ltx')

diff --git a/sec/intro.ltx b/sec/intro.ltx
index 9baaf3f..e60410a 100644
--- a/sec/intro.ltx
+++ b/sec/intro.ltx
@@ -38,15 +38,15 @@ eliminator style to ensure all recursion is structural. If we used
 explicit recursion, we would need complex checks for structural
 recursion, like in Agda~\cite{agda} and Idris~2~\cite{idris}.
 
-As we can encode all \lang{} programs into System~T, \lang{} inherit
+As we can encode all \lang{} programs into System~T, \lang{} inherits
 some of System~T's metatheory for free. In particular, as System~T is
 strongly normalising~\cite{syst-sn}, all \lang{} programs must
-terminate. Requiring programs terminate and are well-founded does not
-appear to greatly restrict what programs you can write in \lang{}. As
-evidence of this, we have written the encoding algorithm from \lang{}
-to System~T within \lang{}. We have also produced a fuelled System~T
-reducer; given enough fuel, it strongly normalises any well-typed
-System~T term.
+terminate. Requiring programs to terminate and use structural
+recursion does not appear to greatly restrict what programs you can
+write in \lang{}. As evidence, we have written the encoding algorithm
+from \lang{} to System~T within \lang{} itself. We have also produced
+a fuelled System~T reducer; given enough fuel, it strongly normalises
+any well-typed System~T term.
 
 Developing these non-trivial recursive programs requires good tools
 for using \lang{}. To that end, we have implemented a certifying type
-- 
cgit v1.2.3

