diff --git a/Appendix/CaseSquash.lhs b/Appendix/CaseSquash.lhs
index 166681c..7f13b88 100644
--- a/Appendix/CaseSquash.lhs
+++ b/Appendix/CaseSquash.lhs
@@ -34,9 +34,9 @@ squashCases :: QName -> TTerm -> TCM TTerm
 squashCases q body = return $ dedupTerm [] body
 \end{code}
 
-Case scrutinee (de Bruijn index) with alternative match
+Case scrutinee (De Bruijn index) with alternative match
 for that expression, made up of qualified name of constructor
-and a list of its arguments (also as de Bruijn indices)
+and a list of its arguments (also as De Bruijn indices)
 
 \begin{code}
 type CaseMatch = (Int, (QName, [Int]))
@@ -103,7 +103,7 @@ dedupAlt sc env (TAGuard guard body) = TAGuard guard (dedupTerm env body)
 dedupAlt sc env (TALit lit body) = TALit lit (dedupTerm env body)
 \end{code}
 
-Shift all de Bruijn indices in a case match according to provided
+Shift all De Bruijn indices in a case match according to provided
 function on integers
 
 \begin{code}
@@ -111,7 +111,7 @@ shiftIndices :: (Int -> Int) -> CaseMatch -> CaseMatch
 shiftIndices f (sc, (name, vars)) = (f sc, (name, map f vars))
 \end{code}
 
-Substitute list of current de Bruijn indices for list of new indices
+Substitute list of current De Bruijn indices for list of new indices
 in a term
 
 \begin{code}
diff --git a/Chapters/CaseSquash.lhs b/Chapters/CaseSquash.lhs
index 7faf6c9..5f92a87 100755
--- a/Chapters/CaseSquash.lhs
+++ b/Chapters/CaseSquash.lhs
@@ -53,7 +53,7 @@ case x of
 \label{fig:case_squash_rule}
 \end{figure}
 
-For example, given the treeless expression with de Bruijn indexed variables in Figure~\ref{fig:db_case_squash}, we can follow the de Bruijn indices to their matching variable bindings, to see that the first and third case expressions are scrutinising the same variable, the one bound by the outermost $\lambda$ abstraction. Therefore, with only static analysis of the expression tree, we know that the third case expression must follow the $da~2~1~0$ branch, and we can thus safely transform the expression on the left into the substituted expression on the right.
+For example, given the treeless expression with De Bruijn indexed variables in Figure~\ref{fig:db_case_squash}, we can follow the De Bruijn indices to their matching variable bindings, to see that the first and third case expressions are scrutinising the same variable, the one bound by the outermost $\lambda$ abstraction. Therefore, with only static analysis of the expression tree, we know that the third case expression must follow the $da~2~1~0$ branch, and we can thus safely transform the expression on the left into the substituted expression on the right.
 
 \begin{figure}[h]
 \centering
@@ -94,7 +94,7 @@ case $2$ of {
 \label{fig:db_case_squash}
 \end{figure}
 
-We perform this ``case squashing'' by accumulating an environment of all previously scrutinised variables as we traverse the tree structure (appropriately shifting de Bruijn indices in the environment as new variables are bound), and replacing case expressions that match on the same variable as an ancestor case expressions, with the corresponding case branch's body. Any variables in the body that refer to bindings in the removed branch should be replaced with references to the bindings in the matching ancestor case expression branch.
+We perform this ``case squashing'' by accumulating an environment of all previously scrutinised variables as we traverse the tree structure (appropriately shifting De Bruijn indices in the environment as new variables are bound), and replacing case expressions that match on the same variable as an ancestor case expressions, with the corresponding case branch's body. Any variables in the body that refer to bindings in the removed branch should be replaced with references to the bindings in the matching ancestor case expression branch.
 
 \section{Implementation}
 \label{sec:squashing_implement}
diff --git a/Chapters/Conclusion.lhs b/Chapters/Conclusion.lhs
index 2e0c59e..456eb88 100755
--- a/Chapters/Conclusion.lhs
+++ b/Chapters/Conclusion.lhs
@@ -40,7 +40,7 @@ a number of weaknesses that warrant consideration.
 A clear weakness of our case squashing optimisation is its isolated
 implementation. Because it was developed as an independent transformation, it
 requires an additional traversal of the treeless terms to execute. Further, some
-of the logic built to deal with the handling of de Bruijn indices would have
+of the logic built to deal with the handling of De Bruijn indices would have
 been avoidable had it been built as part of an existing set of optimisations
 that had similar optimisation helper functions already developed. As presented
 in Subsection~\ref{sub:alternate_case_squash}, an independent version of case
diff --git a/Chapters/GenPlet.lhs b/Chapters/GenPlet.lhs
index 48731f7..c5c8002 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 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.
+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}.
 
diff --git a/Figures/DeBruijn.tex b/Figures/DeBruijn.tex
index 2def2ca..7f94edf 100644
--- a/Figures/DeBruijn.tex
+++ b/Figures/DeBruijn.tex
@@ -11,6 +11,6 @@
 \centering
 \includegraphics[width=4cm]{Figures/DeBruijnIndex}
 
-\caption{An example of a (circumlocutious) identity function as a pure (above) and de Bruijn indexed (below) $\lambda$-calculus expression.}
+\caption{An example of a (circumlocutious) identity function as a pure (above) and De Bruijn indexed (below) $\lambda$-calculus expression.}
 \label{fig:db_example}
 \end{figure}