diff --git a/.gitignore b/.gitignore
index 7140f41..4cf2910 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,3 +18,4 @@ docs/coqdoc
 .lia.cache
 .coq-native
 docs/report/main.tex
+docs/report/abs_defs.tex
diff --git a/docs/report/abs_defs.tex b/docs/report/abs_defs.tex
deleted file mode 100644
index 2d05bb2..0000000
--- a/docs/report/abs_defs.tex
+++ /dev/null
@@ -1,242 +0,0 @@
-% generated by Ott 0.33 from: src/abs.ott
-\newcommand{\ottdrule}[4][]{{\displaystyle\frac{\begin{array}{l}#2\end{array}}{#3}\quad\ottdrulename{#4}}}
-\newcommand{\ottusedrule}[1]{\[#1\]}
-\newcommand{\ottpremise}[1]{ #1 \\}
-\newenvironment{ottdefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]}{}
-\newenvironment{ottfundefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}}
-\newcommand{\ottfunclause}[2]{ #1 \equiv #2 \\}
-\newcommand{\ottnt}[1]{\mathit{#1}}
-\newcommand{\ottmv}[1]{\mathit{#1}}
-\newcommand{\ottkw}[1]{\mathbf{#1}}
-\newcommand{\ottsym}[1]{#1}
-\newcommand{\ottcom}[1]{\text{#1}}
-\newcommand{\ottdrulename}[1]{\textsc{#1}}
-\newcommand{\ottcomplu}[5]{\overline{#1}^{\,#2\in #3 #4 #5}}
-\newcommand{\ottcompu}[3]{\overline{#1}^{\,#2<#3}}
-\newcommand{\ottcomp}[2]{\overline{#1}^{\,#2}}
-\newcommand{\ottgrammartabular}[1]{\begin{supertabular}{llcllllll}#1\end{supertabular}}
-\newcommand{\ottmetavartabular}[1]{\begin{supertabular}{ll}#1\end{supertabular}}
-\newcommand{\ottrulehead}[3]{$#1$ & & $#2$ & & & \multicolumn{2}{l}{#3}}
-\newcommand{\ottprodline}[6]{& & $#1$ & $#2$ & $#3 #4$ & $#5$ & $#6$}
-\newcommand{\ottfirstprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}}
-\newcommand{\ottlongprodline}[2]{& & $#1$ & \multicolumn{4}{l}{$#2$}}
-\newcommand{\ottfirstlongprodline}[2]{\ottlongprodline{#1}{#2}}
-\newcommand{\ottbindspecprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}}
-\newcommand{\ottprodnewline}{\\}
-\newcommand{\ottinterrule}{\\[5.0mm]}
-\newcommand{\ottafterlastrule}{\\}
-\newcommand{\ottmetavars}{
-\ottmetavartabular{
- $ \ottmv{i} ,\, \ottmv{j} ,\, \ottmv{n} $ & \ottcom{index variables (subscripts)} \\
- $ \ottmv{fn} $ & \ottcom{function name} \\
- $ \ottmv{x} ,\, \ottmv{y} $ & \ottcom{variable} \\
- $ \ottmv{b} $ & \ottcom{boolean} \\
- $ \ottmv{z} $ & \ottcom{integer} \\
-}}
-
-\newcommand{\ottT}{
-\ottrulehead{\ottnt{T}}{::=}{\ottcom{ground type}}\ottprodnewline
-\ottfirstprodline{|}{\mathsf{Bool}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\mathsf{Int}}{}{}{}{}}
-
-\newcommand{\ottF}{
-\ottrulehead{\ottnt{F}}{::=}{\ottcom{function definition}}\ottprodnewline
-\ottfirstprodline{|}{\ottkw{def} \, \ottnt{T} \, \ottmv{fn}  \ottsym{(}  \ottnt{T_{{\mathrm{1}}}} \, \ottmv{x_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{T_{\ottmv{n}}} \, \ottmv{x_{\ottmv{n}}}  \ottsym{)}  \ottsym{=}  \ottnt{e}  \ottsym{;}}{}{}{}{}}
-
-\newcommand{\ottt}{
-\ottrulehead{\ottnt{t}}{::=}{\ottcom{ground term}}\ottprodnewline
-\ottfirstprodline{|}{\ottmv{b}}{}{}{}{\ottcom{boolean}}\ottprodnewline
-\ottprodline{|}{\ottmv{z}}{}{}{}{\ottcom{integer}}}
-
-\newcommand{\otte}{
-\ottrulehead{\ottnt{e}}{::=}{\ottcom{expression}}\ottprodnewline
-\ottfirstprodline{|}{\ottnt{t}}{}{}{}{\ottcom{term}}\ottprodnewline
-\ottprodline{|}{\ottmv{x}}{}{}{}{\ottcom{variable}}\ottprodnewline
-\ottprodline{|}{\ottmv{fn}  \ottsym{(}  \ottnt{e_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{e_{\ottmv{n}}}  \ottsym{)}}{}{}{}{\ottcom{function call}}\ottprodnewline
-\ottprodline{|}{\ottnt{e}  \ottsym{[}  \ottmv{x_{{\mathrm{1}}}}  \mapsto  \ottmv{y_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottmv{x_{\ottmv{n}}}  \mapsto  \ottmv{y_{\ottmv{n}}}  \ottsym{]}} {\textsf{M}}{}{}{}}
-
-\newcommand{\ottsig}{
-\ottrulehead{\ottnt{sig}}{::=}{}\ottprodnewline
-\ottfirstprodline{|}{\ottnt{T_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{T_{\ottmv{n}}}  \rightarrow  \ottnt{T}}{}{}{}{}}
-
-\newcommand{\ottctxv}{
-\ottrulehead{\ottnt{ctxv}}{::=}{}\ottprodnewline
-\ottfirstprodline{|}{\ottnt{T}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottnt{sig}}{}{}{}{}}
-
-\newcommand{\ottG}{
-\ottrulehead{\Gamma}{::=}{}\ottprodnewline
-\ottfirstprodline{|}{\Gamma  \ottsym{[}  \ottmv{x_{{\mathrm{1}}}}  \mapsto  \ottnt{T_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottmv{x_{\ottmv{n}}}  \mapsto  \ottnt{T_{\ottmv{n}}}  \ottsym{]}} {\textsf{M}}{}{}{}}
-
-\newcommand{\otts}{
-\ottrulehead{\sigma}{::=}{}\ottprodnewline
-\ottfirstprodline{|}{\sigma  \ottsym{[}  \ottmv{x_{{\mathrm{1}}}}  \mapsto  \ottnt{t_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottmv{x_{\ottmv{n}}}  \mapsto  \ottnt{t_{\ottmv{n}}}  \ottsym{]}} {\textsf{M}}{}{}{}}
-
-\newcommand{\ottterminals}{
-\ottrulehead{\ottnt{terminals}}{::=}{}\ottprodnewline
-\ottfirstprodline{|}{ \mathsf{Bool} }{}{}{}{}\ottprodnewline
-\ottprodline{|}{ \mathsf{Int} }{}{}{}{}\ottprodnewline
-\ottprodline{|}{ \leadsto }{}{}{}{}\ottprodnewline
-\ottprodline{|}{ \vdash }{}{}{}{}\ottprodnewline
-\ottprodline{|}{ \mapsto }{}{}{}{}\ottprodnewline
-\ottprodline{|}{ \rightarrow }{}{}{}{}}
-
-\newcommand{\ottformula}{
-\ottrulehead{\ottnt{formula}}{::=}{}\ottprodnewline
-\ottfirstprodline{|}{\ottnt{judgement}}{}{}{}{\ottcom{judgment}}\ottprodnewline
-\ottprodline{|}{\ottnt{formula_{{\mathrm{1}}}} \quad ... \quad \ottnt{formula_{\ottmv{n}}}}{}{}{}{\ottcom{conjunction of formulas}}\ottprodnewline
-\ottprodline{|}{\Gamma  \ottsym{(}  \ottmv{x}  \ottsym{)}  \ottsym{=}  \ottnt{T}} {\textsf{M}}{}{}{}\ottprodnewline
-\ottprodline{|}{\sigma  \ottsym{(}  \ottmv{x}  \ottsym{)}  \ottsym{=}  \ottnt{t}} {\textsf{M}}{}{}{}\ottprodnewline
-\ottprodline{|}{\Gamma  \ottsym{(}  \ottmv{fn}  \ottsym{)}  \ottsym{=}  \ottnt{sig}} {\textsf{M}}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottkw{fresh} \, \ottsym{(}  \ottmv{x_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottmv{x_{\ottmv{n}}}  \ottsym{,}  \ottnt{e}  \ottsym{)}} {\textsf{M}}{}{}{}}
-
-\newcommand{\ottfunctionalXXwellXXtyping}{
-\ottrulehead{\ottnt{functional\_well\_typing}}{::=}{}\ottprodnewline
-\ottfirstprodline{|}{\Gamma  \vdash  \ottnt{e}  \ottsym{:}  \ottnt{T}}{}{}{}{\ottcom{well-typed expression}}\ottprodnewline
-\ottprodline{|}{\Gamma  \vdash  \ottnt{F}}{}{}{}{\ottcom{well-typed function declaration}}}
-
-\newcommand{\ottfunctionalXXevaluation}{
-\ottrulehead{\ottnt{functional\_evaluation}}{::=}{}\ottprodnewline
-\ottfirstprodline{|}{\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{n}}}  \ottsym{,}  \sigma  \vdash  \ottnt{e}  \leadsto  \sigma'  \vdash  \ottnt{e'}}{}{}{}{\ottcom{expression evaluation}}}
-
-\newcommand{\ottjudgement}{
-\ottrulehead{\ottnt{judgement}}{::=}{}\ottprodnewline
-\ottfirstprodline{|}{\ottnt{functional\_well\_typing}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottnt{functional\_evaluation}}{}{}{}{}}
-
-\newcommand{\ottuserXXsyntax}{
-\ottrulehead{\ottnt{user\_syntax}}{::=}{}\ottprodnewline
-\ottfirstprodline{|}{\ottmv{i}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottmv{fn}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottmv{x}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottmv{b}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottmv{z}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottnt{T}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottnt{F}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottnt{t}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottnt{e}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottnt{sig}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottnt{ctxv}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\Gamma}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\sigma}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottnt{terminals}}{}{}{}{}\ottprodnewline
-\ottprodline{|}{\ottnt{formula}}{}{}{}{}}
-
-\newcommand{\ottgrammar}{\ottgrammartabular{
-\ottT\ottinterrule
-\ottF\ottinterrule
-\ottt\ottinterrule
-\otte\ottinterrule
-\ottsig\ottinterrule
-\ottctxv\ottinterrule
-\ottG\ottinterrule
-\otts\ottinterrule
-\ottterminals\ottinterrule
-\ottformula\ottinterrule
-\ottfunctionalXXwellXXtyping\ottinterrule
-\ottfunctionalXXevaluation\ottinterrule
-\ottjudgement\ottinterrule
-\ottuserXXsyntax\ottafterlastrule
-}}
-
-% defnss
-% defns functional_well_typing
-%% defn e
-\newcommand{\ottdruletypXXbool}[1]{\ottdrule[#1]{%
-}{
-\Gamma  \vdash  \ottmv{b}  \ottsym{:}  \mathsf{Bool}}{%
-{\ottdrulename{typ\_bool}}{}%
-}}
-
-
-\newcommand{\ottdruletypXXint}[1]{\ottdrule[#1]{%
-}{
-\Gamma  \vdash  \ottmv{z}  \ottsym{:}  \mathsf{Int}}{%
-{\ottdrulename{typ\_int}}{}%
-}}
-
-
-\newcommand{\ottdruletypXXvar}[1]{\ottdrule[#1]{%
-\ottpremise{\Gamma  \ottsym{(}  \ottmv{x}  \ottsym{)}  \ottsym{=}  \ottnt{T}}%
-}{
-\Gamma  \vdash  \ottmv{x}  \ottsym{:}  \ottnt{T}}{%
-{\ottdrulename{typ\_var}}{}%
-}}
-
-
-\newcommand{\ottdruletypXXfuncXXexpr}[1]{\ottdrule[#1]{%
-\ottpremise{\Gamma  \vdash  \ottnt{e_{{\mathrm{1}}}}  \ottsym{:}  \ottnt{T_{{\mathrm{1}}}} \quad ... \quad \Gamma  \vdash  \ottnt{e_{\ottmv{n}}}  \ottsym{:}  \ottnt{T_{\ottmv{n}}}}%
-\ottpremise{\Gamma  \ottsym{(}  \ottmv{fn}  \ottsym{)}  \ottsym{=}  \ottnt{T_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{T_{\ottmv{n}}}  \rightarrow  \ottnt{T}}%
-}{
-\Gamma  \vdash  \ottmv{fn}  \ottsym{(}  \ottnt{e_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{e_{\ottmv{n}}}  \ottsym{)}  \ottsym{:}  \ottnt{T}}{%
-{\ottdrulename{typ\_func\_expr}}{}%
-}}
-
-\newcommand{\ottdefntypXXe}[1]{\begin{ottdefnblock}[#1]{$\Gamma  \vdash  \ottnt{e}  \ottsym{:}  \ottnt{T}$}{\ottcom{well-typed expression}}
-\ottusedrule{\ottdruletypXXbool{}}
-\ottusedrule{\ottdruletypXXint{}}
-\ottusedrule{\ottdruletypXXvar{}}
-\ottusedrule{\ottdruletypXXfuncXXexpr{}}
-\end{ottdefnblock}}
-
-%% defn F
-\newcommand{\ottdruletypXXfuncXXdecl}[1]{\ottdrule[#1]{%
-\ottpremise{\Gamma  \ottsym{(}  \ottmv{fn}  \ottsym{)}  \ottsym{=}  \ottnt{T_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{T_{\ottmv{n}}}  \rightarrow  \ottnt{T}}%
-\ottpremise{\Gamma  \ottsym{[}  \ottmv{x_{{\mathrm{1}}}}  \mapsto  \ottnt{T_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottmv{x_{\ottmv{n}}}  \mapsto  \ottnt{T_{\ottmv{n}}}  \ottsym{]}  \vdash  \ottnt{e}  \ottsym{:}  \ottnt{T}}%
-}{
-\Gamma  \vdash  \ottkw{def} \, \ottnt{T} \, \ottmv{fn}  \ottsym{(}  \ottnt{T_{{\mathrm{1}}}} \, \ottmv{x_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{T_{\ottmv{n}}} \, \ottmv{x_{\ottmv{n}}}  \ottsym{)}  \ottsym{=}  \ottnt{e}  \ottsym{;}}{%
-{\ottdrulename{typ\_func\_decl}}{}%
-}}
-
-\newcommand{\ottdefntypXXF}[1]{\begin{ottdefnblock}[#1]{$\Gamma  \vdash  \ottnt{F}$}{\ottcom{well-typed function declaration}}
-\ottusedrule{\ottdruletypXXfuncXXdecl{}}
-\end{ottdefnblock}}
-
-
-\newcommand{\ottdefnsfunctionalXXwellXXtyping}{
-\ottdefntypXXe{}\ottdefntypXXF{}}
-
-% defns functional_evaluation
-%% defn e
-\newcommand{\ottdruleredXXvar}[1]{\ottdrule[#1]{%
-\ottpremise{\sigma  \ottsym{(}  \ottmv{x}  \ottsym{)}  \ottsym{=}  \ottnt{t}}%
-}{
-\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{n}}}  \ottsym{,}  \sigma  \vdash  \ottmv{x}  \leadsto  \sigma  \vdash  \ottnt{t}}{%
-{\ottdrulename{red\_var}}{}%
-}}
-
-
-\newcommand{\ottdruleredXXfunXXexp}[1]{\ottdrule[#1]{%
-\ottpremise{\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{n}}}  \ottsym{,}  \sigma  \vdash  \ottnt{e}  \leadsto  \sigma'  \vdash  \ottnt{e'}}%
-}{
-\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{n}}}  \ottsym{,}  \sigma  \vdash  \ottmv{fn}  \ottsym{(}  \ottnt{e_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{e_{\ottmv{i}}}  \ottsym{,}  \ottnt{e}  \ottsym{,}  \ottnt{e'_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{e'_{\ottmv{j}}}  \ottsym{)}  \leadsto  \sigma'  \vdash  \ottmv{fn}  \ottsym{(}  \ottnt{e_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{e_{\ottmv{i}}}  \ottsym{,}  \ottnt{e'}  \ottsym{,}  \ottnt{e'_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{e'_{\ottmv{j}}}  \ottsym{)}}{%
-{\ottdrulename{red\_fun\_exp}}{}%
-}}
-
-
-\newcommand{\ottdruleredXXfunXXground}[1]{\ottdrule[#1]{%
-\ottpremise{\ottkw{fresh} \, \ottsym{(}  \ottmv{y_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottmv{y_{\ottmv{n}}}  \ottsym{,}  \ottnt{e}  \ottsym{)}}%
-}{
-\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{i}}} \, \ottkw{def} \, \ottnt{T} \, \ottmv{fn}  \ottsym{(}  \ottnt{T_{{\mathrm{1}}}} \, \ottmv{x_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{T_{\ottmv{n}}} \, \ottmv{x_{\ottmv{n}}}  \ottsym{)}  \ottsym{=}  \ottnt{e}  \ottsym{;} \, \ottnt{F'_{{\mathrm{1}}}} \, ... \, \ottnt{F'_{\ottmv{j}}}  \ottsym{,}  \sigma  \vdash  \ottmv{fn}  \ottsym{(}  \ottnt{t_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottnt{t_{\ottmv{n}}}  \ottsym{)}  \leadsto  \sigma  \ottsym{[}  \ottmv{y_{{\mathrm{1}}}}  \mapsto  \ottnt{t_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottmv{y_{\ottmv{n}}}  \mapsto  \ottnt{t_{\ottmv{n}}}  \ottsym{]}  \vdash  \ottnt{e}  \ottsym{[}  \ottmv{x_{{\mathrm{1}}}}  \mapsto  \ottmv{y_{{\mathrm{1}}}}  \ottsym{,} \, ... \, \ottsym{,}  \ottmv{x_{\ottmv{n}}}  \mapsto  \ottmv{y_{\ottmv{n}}}  \ottsym{]}}{%
-{\ottdrulename{red\_fun\_ground}}{}%
-}}
-
-\newcommand{\ottdefnredXXe}[1]{\begin{ottdefnblock}[#1]{$\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{n}}}  \ottsym{,}  \sigma  \vdash  \ottnt{e}  \leadsto  \sigma'  \vdash  \ottnt{e'}$}{\ottcom{expression evaluation}}
-\ottusedrule{\ottdruleredXXvar{}}
-\ottusedrule{\ottdruleredXXfunXXexp{}}
-\ottusedrule{\ottdruleredXXfunXXground{}}
-\end{ottdefnblock}}
-
-
-\newcommand{\ottdefnsfunctionalXXevaluation}{
-\ottdefnredXXe{}}
-
-\newcommand{\ottdefnss}{
-\ottdefnsfunctionalXXwellXXtyping
-\ottdefnsfunctionalXXevaluation
-}
-
-\newcommand{\ottall}{\ottmetavars\\[0pt]
-\ottgrammar\\[5.0mm]
-\ottdefnss}
-
diff --git a/docs/report/main.mng b/docs/report/main.mng
index 7512b95..afb1ee6 100644
--- a/docs/report/main.mng
+++ b/docs/report/main.mng
@@ -85,6 +85,18 @@ In this section, we define the semantics of ABS.
 
 In this section, we define the metatheory of ABS.
 
+\begin{definition}
+A context $[[G']]$ subsumes context $[[G]]$, written $[[G]] \subseteq [[G']]$, if whenever $[[G(x) = T]]$ then $[[G'(x) = T]]$ and whenever $[[G(fn) = sig]]$ then $[[G'(fn) = sig]]$.
+\end{definition}
+
+\begin{definition}
+A context $[[G]]$ is consistent with a substitutition $[[s]]$, written $[[G]] \vdash [[s]]$.
+\end{definition}
+
+\begin{theorem}[Type preservation]
+Assume $[[G]] \vdash [[s]]$
+\end{theorem}
+
 \bibliographystyle{abbrv}
 \bibliography{bib}