From 2eaa70248abba984b17a422855406c28c9076bf4 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 15:11:29 +0100
Subject: Fix 721--727.

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

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index c87ce90..fa40ec0 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -494,7 +494,7 @@ let dupfirst t = fun x => match x with
 \subsection{Phase 6: Encoding Unions}%
 \label{subsec:unions}
 
-At this point, the only type former we use that is not present in
+At this phase the only type former we use that is not present in
 System~T is the union type.\@ \textcite{oleg} gives an inductive
 encoding for binary unions. We instead use an encoding for unions
 derived from the argument form of types. Given we have a family of
-- 
cgit v1.2.3

