diff --git a/Chapters/GenPlet.lhs b/Chapters/GenPlet.lhs
index 64e2a71..44fed81 100755
--- a/Chapters/GenPlet.lhs
+++ b/Chapters/GenPlet.lhs
@@ -60,7 +60,7 @@ These generated pattern lets have two-fold benefits. Firstly, their use reduces
 \section{Implementation}
 \label{sec:plet_implement}
 
-The |Agda.Compiler.MAlonzo.Compiler| module is responsible for transforming Agda treeless terms into Haskell expressions. In the primary function for this compilation, we introduced a new alternative that matches on terms with potential to be transformed into pattern lets. In order to be a suitable candidate for this optimisation, a |let| expression must exhibit the properties described in Section~\ref{sec:plet_logical}. Because these Agda terms used de Bruijn indexed variables, that means the case expression should be scrutinising the 0 (most recently bound) variable, and the requirements can thus be represented with a pattern matching expression |TLet _ (TCase 0 _ _ [TACon _ _ _])|, followed by a check that the default branch is unreachable.
+The |Agda.Compiler.MAlonzo.Compiler| module is responsible for transforming Agda treeless terms into Haskell expressions. In the primary function for this compilation, we introduced a new alternative that matches on terms with potential to be transformed into pattern lets. In order to be a suitable candidate for this optimisation, a |let| expression must exhibit the properties described in Section~\ref{sec:plet_logical}. Because these Agda terms use de Bruijn indexed variables, that means the case expression should be scrutinising the 0 (most recently bound) variable, and the requirements can thus be represented with a pattern matching expression |TLet _ (TCase 0 _ _ [TACon _ _ _])|, followed by a check that the default branch is unreachable.
 
 For a complete listing of our implementation of the pattern let generating optimisation, refer to Appendix~\ref{app:compiler}.