Fix 31--37.

1 files changed, 7 insertions, 7 deletions

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