diff --git a/cbpv.bib b/cbpv.bib
index e69de29..762c4e2 100644
--- a/cbpv.bib
+++ b/cbpv.bib
@@ -0,0 +1,41 @@
+@inproceedings{cbpv,
+  author = {Forster, Yannick and Sch\"{a}fer, Steven and Spies, Simon and Stark, Kathrin},
+  title = {{Call-by-push-value in Coq: operational, equational, and denotational theory}},
+  year = 2019,
+  isbn = {9781450362221},
+  publisher = {Association for Computing Machinery},
+  address = {New York, NY, USA},
+  doi = {10.1145/3293880.3294097},
+  booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+  pages = {118--131},
+  numpages = {14},
+  location = {Cascais, Portugal},
+  series = {CPP 2019}
+}
+
+@article{poplmark,
+  title = {{POPLMark reloaded: Mechanizing proofs by logical relations}},
+  volume = 29,
+  DOI = {10.1017/S0956796819000170},
+  journal = {Journal of Functional Programming},
+  publisher = {Cambridge University Press},
+  author = {Abel, Andreas and Allais, Guillaume and Hameer, Aliya and Pientka, Brigitte and Momigliano, Alberto and Schäfer, Steven and Stark, Kathrin},
+  year = 2019,
+  pages = {e19}
+}
+
+@inproceedings{autosubst2,
+  author = {Stark, Kathrin and Sch\"{a}fer, Steven and Kaiser, Jonas},
+  title = {{Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions}},
+  year = 2019,
+  isbn = {9781450362221},
+  publisher = {Association for Computing Machinery},
+  address = {New York, NY, USA},
+  doi = {10.1145/3293880.3294101},
+  booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs},
+  pages = {166--180},
+  numpages = 15,
+  keywords = {de Bruijn repersentation, multi-sorted terms, parallel substiutions, sigma-calculus},
+  location = {Cascais, Portugal},
+  series = {CPP 2019}
+}
\ No newline at end of file
diff --git a/cbpv.mng b/cbpv.mng
index 477ccee..0f9dca8 100644
--- a/cbpv.mng
+++ b/cbpv.mng
@@ -3,13 +3,14 @@
 \usepackage[supertabular]{ottalt}
 \let\newlist\relax
 \let\renewlist\relax
+\usepackage[margin=1in]{geometry}
 \usepackage[T1]{fontenc}
 \usepackage{mlmodern}
-\usepackage[margin=1in]{geometry}
-\usepackage{enumitem,float,booktabs,xspace,doi}
+\usepackage{enumitem,float,booktabs,xspace,xcolor,doi}
 \usepackage{amsmath,amsthm,amssymb}
-\usepackage[capitalize,nameinlink,noabbrev]{cleveref}
 \usepackage{mathpartir,mathtools,stmaryrd,latexsym}
+\usepackage[capitalize,nameinlink,noabbrev]{cleveref}
+\usepackage[numbers]{natbib}
 
 \setlist{noitemsep}
 \hypersetup{
@@ -43,8 +44,8 @@
 \section{Introduction}
 
 The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV).
-It follows work by Forster, Sch\"afer, Spies, and Stark (TODO: cite) on mechanizing the metatheory of CBPV in Rocq,
-but instead adapts the proof technique from POPLMark Reloaded (TODO: cite).
+It follows work by Forster, Sch\"afer, Spies, and Stark \citep{cbpv} on mechanizing the metatheory of CBPV in Rocq,
+but instead adapts the proof technique from POPLMark Reloaded \citep{poplmark}.
 
 Both proofs, and mine, follow the same sequence of steps:
 we define a logical relation that semantically interpret types as sets of terms,
@@ -60,7 +61,8 @@ In contrast to both prior works, which use Rocq, Agda, or Beluga,
 this project is mechanized in Lean.
 A secondary purpose of this project is to assess the capabilities of Lean for PL metatheory,
 especially when making heavy use of mutually defined inductive types.
-I have implemented a mutual induction tactic for Lean (TODO: link),
+I have implemented a mutual induction tactic for Lean%
+\footnote{\url{https://github.com/ionathanch/MutualInduction}},
 and the mutual values and computations of CBPV,
 combined with the even more complex mutual inductives from POPLMark Reloaded,
 make it an attractive test case to test the tactic's robustness.
@@ -301,7 +303,7 @@ match on the term and the type and returning the conjunction of its premises,
 but I wanted to use a mutually defined inductive definition.
 
 \begin{figure}[H]
-\fbox{$[[v ∈ ⟦A⟧]]$} \quad \fbox{$[[m ∈ ⟦B⟧]]$} \hfill \textit{} \\
+\fbox{$[[v ∈ ⟦A⟧]]$} \quad \fbox{$[[m ∈ ⟦B⟧]]$} \hfill \textit{semantic inhabitance of types} \\
 \begin{mathpar}
 \drule[]{LRPP-Unit-var}
 \drule[]{LRPP-Unit-unit}
@@ -716,6 +718,8 @@ traditional strong normalization of well typed terms holds as a corollary.
 
 \section{Discussion} \label{sec:discussion}
 
+\subsection{Proof Structure of Strong Normalization}
+
 Overall, the inductive characterization of strongly normal terms is convenient to work with.
 Its congruence and inversion properties are exactly what are needed
 to show \nameref{lem:closure} and \nameref{lem:adequacy} of the logical relation,
@@ -797,4 +801,122 @@ to the particularities of the chosen reduction strategy.
 
 \subsection{Lean for PL Metatheory}
 
+The proof development involved in this report consists of nine files,
+as mentioned throughout.
+\Cref{tab:loc} gives the number of non-blank, non-comment lines of code for each file,
+which roughly reflects the amount of proof effort I required.
+The \texttt{Syntax.lean} file involves a lot of renaming and substitution proofs,
+but I copied these from prior proof developments with minimal changes to adapt them to CBPV.
+The actual semantic proofs in \texttt{NormalInd.lean}, \texttt{OpenSemantics.lean}, and \texttt{Soundness.lean}
+took roughly equal amounts of time to complete.
+As said in \cref{sec:sn-acc}, the proofs in \texttt{NormalAcc.lean}
+along with its dependency on \texttt{Reduction.lean} took nearly as much time to complete
+as the rest of the semantic proofs,
+while \texttt{LeftmostOutermost.lean} mostly mirrors \texttt{Reduction.lean}.
+The entire project, excluding this report, took about a week to complete.
+
+\begin{table}[H]
+\centering
+\begin{tabular}{lr}
+  \toprule
+  File & LOC \\
+  \midrule
+  \texttt{Syntax.lean}            & 252 \\
+  \texttt{Typing.lean}            &  48 \\
+  \texttt{NormalInd.lean}         & 192 \\
+  \texttt{OpenSemantics.lean}     & 107 \\
+  \texttt{Soundness.lean}         & 114 \\
+  \texttt{Normalization.lean}     &  48 \\
+  \texttt{Reduction.lean}         & 187 \\
+  \texttt{NormalAcc.lean}         & 291 \\
+  \texttt{LeftmostOutermost.lean} & 276 \\
+  \bottomrule
+\end{tabular}
+\caption{Lean development files and lines of code}
+\label{tab:loc}
+\end{table}
+
+One of the main technical challenges in mechanizing CBPV in Lean is dealing with mutual induction.
+While Lean currently supports mutually defined inductive types,
+the options for eliminating them are somewhat buggy and restricted.
+At the lower level,
+Lean generates independent eliminators (which they call \emph{recursors})
+for each of the mutual inductives,
+each with motives for all mutual inductives,
+similar to what \texttt{Scheme Induction for ... with Induction for ...}
+generates in Rocq.
+
+Lean's induction tactic produces applications of the appropriate recursor,
+but does not support mutual inductives.
+In cases where induction on only a single inductive from the mutual definitions is needed,
+the induction tactic can be supplied with a custom recursor,
+in this case the appropriate inductive's recursor with all other motives
+instantiated to trivial propositions.
+Unfortunately, this fails because the tactic cannot handle induction cases
+with different numbers of indices in the inductive type,
+even if those other cases are eventually trivial.
+
+Lean supports structural recursion on mutual inductives,
+which is implemented via a recursor on an auxiliary inductive
+that enables strong induction.
+However, this feature is currently a little buggy,
+and fails on some more complex inductive types.%
+\footnote{\url{https://github.com/leanprover/lean4/issues/1672}}
+Futhermore, writing proofs as recursive functions is unconventional,
+and isn't amenable to even simple automation that can automatically apply induction hypotheses.
+
+Of course, it's possible to manually apply the recursors that Lean generates for each mutual inductive.
+This is inconvenient for several reasons:
+motives need to be explicitly specified, even when they're inferrable from the goals;
+cases with trivial motives still need to be explicitly proven;
+and induction cases are duplicated across the recursors.
+A partial solution, especially for the last inconvenience,
+is to generate the same kind of combined recursor that \texttt{Combined Scheme ...}
+does for Rocq, but it still requires explicit application.
+The mutual induction tactic I had implemented (outside of this project)
+aims to solve these issues.
+
+In short, my mutual induction tactic targets multiple goals at a time.
+Applying the tactic on targets in mutually defined inductives from different goals
+applies their respective recursors, inferring motives from those goals,
+but deduplicates the induction cases, and introduces these cases as new subgoals.
+If a target and goal for a particular inductive is missing,
+the motive for that inductive is set as a trivially inhabited type,
+and all cases for that motive are automatically solved.
+
+The mutual induction tactic has worked very well for this project.
+The mutual inductives involved are the value and computation terms and types (2 and 2),
+their typing judgements (2), the logical relation (2),
+the small-step reduction relation (2),
+and the mutually inductive definition of strongly neutral and normal terms and head reduction (4).
+The tactic was used for every proof by mutual induction mentioned here.
+Additionally, it was used twice for single induction
+(\ie all other motives are trivial): \rref{SN-Force-inv} and \nameref{cor:ext}.
+
+Because the mutual induction tactic is merely a tactic and not a top-level construct,
+some amount of manipulation is still required to massage the proof state
+into one where the tactic can be used.
+Specifically, mutual theorems are first stated as some conjunction
+$(\forall v, P \gap v) \wedge (\forall m, Q \gap m)$,
+then split into two separate goals with targets $v, m$ introduced into the context,
+before mutual induction is applied to $v$ and $m$ with inferred motives $P$ and $Q$.
+This means that using the theorems individually requires projecting from the conjunction.
+There are discussions underway for introducing top-level syntax for mutual theorems,
+similar to Rocq's \texttt{Theorem ... with ...} vernacular,
+so that multiple goals are introduced automatically with their hypotheses.%
+\footnote{\url{https://leanprover.zulipchat.com/\#narrow/channel/239415-metaprogramming-.2F-tactics/topic/mutual.20induction.20tactic/near/504421657}}
+
+Aside from mutual induction,
+the other technical challenge is proving all the renaming and substitution lemmas.
+There is no library like Autosubst 2 \citep{autosubst2} to automate defining and proving these lemmas.
+In multiple places, substitutions need to be massaged into different propositionally equal forms,
+and this massaging requires knowing exactly what equality is needed.
+For PL metatheory that doesn't involve mutual definitions
+but does involve some notion of binding and abstraction,
+the lack of a library for substitution automation is perhaps the biggest barrier
+to Lean being used for PL.
+
+\bibliographystyle{abbrvnat}
+\bibliography{cbpv.bib}
+
 \end{document}
\ No newline at end of file
diff --git a/cbpv.pdf b/cbpv.pdf
index 1aab7c1..0ceb2fd 100644
--- a/cbpv.pdf
+++ b/cbpv.pdf
@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:43e5d9c6bf7221c1bf6b13b800b398b31fc0f9b82851c485d804852424e7eb21
-size 280430
+oid sha256:9f945624690e80f0ebb4c6c5de7a7af8f953b9aab918c08c3c9e9738bf81e976
+size 320767
diff --git a/cbpv.tex b/cbpv.tex
index 9ea858f..44031ff 100644
--- a/cbpv.tex
+++ b/cbpv.tex
@@ -3,13 +3,14 @@
 \usepackage[supertabular]{ottalt}
 \let\newlist\relax
 \let\renewlist\relax
+\usepackage[margin=1in]{geometry}
 \usepackage[T1]{fontenc}
 \usepackage{mlmodern}
-\usepackage[margin=1in]{geometry}
-\usepackage{enumitem,float,booktabs,xspace,doi}
+\usepackage{enumitem,float,booktabs,xspace,xcolor,doi}
 \usepackage{amsmath,amsthm,amssymb}
-\usepackage[capitalize,nameinlink,noabbrev]{cleveref}
 \usepackage{mathpartir,mathtools,stmaryrd,latexsym}
+\usepackage[capitalize,nameinlink,noabbrev]{cleveref}
+\usepackage[numbers]{natbib}
 
 \setlist{noitemsep}
 \hypersetup{
@@ -43,8 +44,8 @@
 \section{Introduction}
 
 The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV).
-It follows work by Forster, Sch\"afer, Spies, and Stark (TODO: cite) on mechanizing the metatheory of CBPV in Rocq,
-but instead adapts the proof technique from POPLMark Reloaded (TODO: cite).
+It follows work by Forster, Sch\"afer, Spies, and Stark \citep{cbpv} on mechanizing the metatheory of CBPV in Rocq,
+but instead adapts the proof technique from POPLMark Reloaded \citep{poplmark}.
 
 Both proofs, and mine, follow the same sequence of steps:
 we define a logical relation that semantically interpret types as sets of terms,
@@ -60,7 +61,8 @@ In contrast to both prior works, which use Rocq, Agda, or Beluga,
 this project is mechanized in Lean.
 A secondary purpose of this project is to assess the capabilities of Lean for PL metatheory,
 especially when making heavy use of mutually defined inductive types.
-I have implemented a mutual induction tactic for Lean (TODO: link),
+I have implemented a mutual induction tactic for Lean%
+\footnote{\url{https://github.com/ionathanch/MutualInduction}},
 and the mutual values and computations of CBPV,
 combined with the even more complex mutual inductives from POPLMark Reloaded,
 make it an attractive test case to test the tactic's robustness.
@@ -301,7 +303,7 @@ match on the term and the type and returning the conjunction of its premises,
 but I wanted to use a mutually defined inductive definition.
 
 \begin{figure}[H]
-\fbox{$ \ottnt{v}  \in \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} $} \quad \fbox{$ \ottnt{m}  \in \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} $} \hfill \textit{} \\
+\fbox{$ \ottnt{v}  \in \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} $} \quad \fbox{$ \ottnt{m}  \in \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} $} \hfill \textit{semantic inhabitance of types} \\
 \begin{mathpar}
 \drule[]{LRPP-Unit-var}
 \drule[]{LRPP-Unit-unit}
@@ -716,6 +718,8 @@ traditional strong normalization of well typed terms holds as a corollary.
 
 \section{Discussion} \label{sec:discussion}
 
+\subsection{Proof Structure of Strong Normalization}
+
 Overall, the inductive characterization of strongly normal terms is convenient to work with.
 Its congruence and inversion properties are exactly what are needed
 to show \nameref{lem:closure} and \nameref{lem:adequacy} of the logical relation,
@@ -797,4 +801,122 @@ to the particularities of the chosen reduction strategy.
 
 \subsection{Lean for PL Metatheory}
 
+The proof development involved in this report consists of nine files,
+as mentioned throughout.
+\Cref{tab:loc} gives the number of non-blank, non-comment lines of code for each file,
+which roughly reflects the amount of proof effort I required.
+The \texttt{Syntax.lean} file involves a lot of renaming and substitution proofs,
+but I copied these from prior proof developments with minimal changes to adapt them to CBPV.
+The actual semantic proofs in \texttt{NormalInd.lean}, \texttt{OpenSemantics.lean}, and \texttt{Soundness.lean}
+took roughly equal amounts of time to complete.
+As said in \cref{sec:sn-acc}, the proofs in \texttt{NormalAcc.lean}
+along with its dependency on \texttt{Reduction.lean} took nearly as much time to complete
+as the rest of the semantic proofs,
+while \texttt{LeftmostOutermost.lean} mostly mirrors \texttt{Reduction.lean}.
+The entire project, excluding this report, took about a week to complete.
+
+\begin{table}[H]
+\centering
+\begin{tabular}{lr}
+  \toprule
+  File & LOC \\
+  \midrule
+  \texttt{Syntax.lean}            & 252 \\
+  \texttt{Typing.lean}            &  48 \\
+  \texttt{NormalInd.lean}         & 192 \\
+  \texttt{OpenSemantics.lean}     & 107 \\
+  \texttt{Soundness.lean}         & 114 \\
+  \texttt{Normalization.lean}     &  48 \\
+  \texttt{Reduction.lean}         & 187 \\
+  \texttt{NormalAcc.lean}         & 291 \\
+  \texttt{LeftmostOutermost.lean} & 276 \\
+  \bottomrule
+\end{tabular}
+\caption{Lean development files and lines of code}
+\label{tab:loc}
+\end{table}
+
+One of the main technical challenges in mechanizing CBPV in Lean is dealing with mutual induction.
+While Lean currently supports mutually defined inductive types,
+the options for eliminating them are somewhat buggy and restricted.
+At the lower level,
+Lean generates independent eliminators (which they call \emph{recursors})
+for each of the mutual inductives,
+each with motives for all mutual inductives,
+similar to what \texttt{Scheme Induction for ... with Induction for ...}
+generates in Rocq.
+
+Lean's induction tactic produces applications of the appropriate recursor,
+but does not support mutual inductives.
+In cases where induction on only a single inductive from the mutual definitions is needed,
+the induction tactic can be supplied with a custom recursor,
+in this case the appropriate inductive's recursor with all other motives
+instantiated to trivial propositions.
+Unfortunately, this fails because the tactic cannot handle induction cases
+with different numbers of indices in the inductive type,
+even if those other cases are eventually trivial.
+
+Lean supports structural recursion on mutual inductives,
+which is implemented via a recursor on an auxiliary inductive
+that enables strong induction.
+However, this feature is currently a little buggy,
+and fails on some more complex inductive types.%
+\footnote{\url{https://github.com/leanprover/lean4/issues/1672}}
+Futhermore, writing proofs as recursive functions is unconventional,
+and isn't amenable to even simple automation that can automatically apply induction hypotheses.
+
+Of course, it's possible to manually apply the recursors that Lean generates for each mutual inductive.
+This is inconvenient for several reasons:
+motives need to be explicitly specified, even when they're inferrable from the goals;
+cases with trivial motives still need to be explicitly proven;
+and induction cases are duplicated across the recursors.
+A partial solution, especially for the last inconvenience,
+is to generate the same kind of combined recursor that \texttt{Combined Scheme ...}
+does for Rocq, but it still requires explicit application.
+The mutual induction tactic I had implemented (outside of this project)
+aims to solve these issues.
+
+In short, my mutual induction tactic targets multiple goals at a time.
+Applying the tactic on targets in mutually defined inductives from different goals
+applies their respective recursors, inferring motives from those goals,
+but deduplicates the induction cases, and introduces these cases as new subgoals.
+If a target and goal for a particular inductive is missing,
+the motive for that inductive is set as a trivially inhabited type,
+and all cases for that motive are automatically solved.
+
+The mutual induction tactic has worked very well for this project.
+The mutual inductives involved are the value and computation terms and types (2 and 2),
+their typing judgements (2), the logical relation (2),
+the small-step reduction relation (2),
+and the mutually inductive definition of strongly neutral and normal terms and head reduction (4).
+The tactic was used for every proof by mutual induction mentioned here.
+Additionally, it was used twice for single induction
+(\ie all other motives are trivial): \rref{SN-Force-inv} and \nameref{cor:ext}.
+
+Because the mutual induction tactic is merely a tactic and not a top-level construct,
+some amount of manipulation is still required to massage the proof state
+into one where the tactic can be used.
+Specifically, mutual theorems are first stated as some conjunction
+$(\forall v, P \gap v) \wedge (\forall m, Q \gap m)$,
+then split into two separate goals with targets $v, m$ introduced into the context,
+before mutual induction is applied to $v$ and $m$ with inferred motives $P$ and $Q$.
+This means that using the theorems individually requires projecting from the conjunction.
+There are discussions underway for introducing top-level syntax for mutual theorems,
+similar to Rocq's \texttt{Theorem ... with ...} vernacular,
+so that multiple goals are introduced automatically with their hypotheses.%
+\footnote{\url{https://leanprover.zulipchat.com/\#narrow/channel/239415-metaprogramming-.2F-tactics/topic/mutual.20induction.20tactic/near/504421657}}
+
+Aside from mutual induction,
+the other technical challenge is proving all the renaming and substitution lemmas.
+There is no library like Autosubst 2 \citep{autosubst2} to automate defining and proving these lemmas.
+In multiple places, substitutions need to be massaged into different propositionally equal forms,
+and this massaging requires knowing exactly what equality is needed.
+For PL metatheory that doesn't involve mutual definitions
+but does involve some notion of binding and abstraction,
+the lack of a library for substitution automation is perhaps the biggest barrier
+to Lean being used for PL.
+
+\bibliographystyle{abbrvnat}
+\bibliography{cbpv.bib}
+
 \end{document}
\ No newline at end of file