Fix 428--437.

1 files changed, 4 insertions, 4 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 822e47a..9f13f1c 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -56,7 +56,7 @@ inductive components.
 Collecting all the inductive components into one location will make
 future encoding steps much easier. We enforce this by removing the
 \roll{} operator and adding the \roll*{} operator, which has the
-following type derivation:
+following typing judgement.
 \[
 \begin{prooftree}
   \hypo{\judgement{\Gamma}{t}{\mathsf{List}~(\mu X.A)}}
@@ -65,9 +65,9 @@ following type derivation:
 \end{prooftree}
 \]
 Rather than including the inductive components within the argument of
-\roll{}, they are instead gathered into an external list. The vessel
-\(u\) now contains pointers to the inductive components within
-\(t\). The new operator satisfies the following equation:
+\roll{}, we instead collect them into an external list. We fill the
+vessel \(u\) with pointers to the values within \(t\). The new
+operator satisfies the following equation:
 \[
 \dofold{\roll*~t~u}{x}{v} \coloneq \sub{v}{x/\mapkw{}~(\lambda i. \dofold{\mathsf{index}~t~i}{x}{v})~u}
 \]