\section{Proof State}

\subsection{Tactics}

\subsection{Unification}

\subsection{The Elaboration DSL}