some initial metatheory statements

.gitignore

@@ -18,3 +18,4 @@ docs/coqdoc
 .lia.cache
 .coq-native
 docs/report/main.tex
+docs/report/abs_defs.tex

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}