Fix 422--427.

1 files changed, 8 insertions, 8 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index e7dfd96..822e47a 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -44,14 +44,14 @@ types.
 \subsection{Phase 1: Simplifying Roll}%
 \label{subsec:simplify-roll}
 
-Recall the typing judgement for \roll{} in \cref{fig:lang-ty}. The
-argument has type \(\sub{A}{X/\mu X. A}\). One consequence of the use of
-substitution is that inductive components can appear scattered
-throughout a vessel of this type. Take the inductive type \(\mu
-X. \lgroup (1 + \nat \times X + \mu Y. (1 + X \times Y)) \times (1 + X) \rgroup\). The
-inductive parameter \(X\) appers in three seperate locations,
-including within another inductive type. A vessel of this shape could
-have any number of inductive components.
+Recall the typing judgement for \roll{} in \cref{M-fig:lang-ty}. The
+argument has type \(\sub{A}{X/\mu X. A}\). Using substitution means that
+inductive components can appear scattered throughout a vessel of this
+type. Take the inductive type \(\mu X. \lgroup (1 + \nat \times X + \mu Y. (1 +
+X \times Y)) \times (1 + X) \rgroup\) as an example. The inductive parameter
+\(X\) appears in three seperate locations, including within another
+inductive type. A vessel of this shape could have any number of
+inductive components.
 
 Collecting all the inductive components into one location will make
 future encoding steps much easier. We enforce this by removing the