@@ -190,7 +190,7 @@ be implemented in the usual way~\cite{loh2010tutorial}.
190190{\Gamma\vdash\vx\Hab\vS}
191191\hg
192192\mathsf{Val}\:
193−\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}
193+\Rule{(\LET\:\vx\defq\vs\Hab\vS)\in\Gamma}
194194{\Gamma\vdash\vx\Hab\vS}
195195\\
196196\mathsf{App}\:
@@ -476,29 +476,49 @@ trees~\cite{Augustsson1985}.
476476\subsection{Metatheory}
477477
478478\FFIG{
479−\AR{
480−\mbox{\textbf{TODO}}\\
481−\mbox{Church-Rosser}
479+\begin{array}{ll}
480+\mbox{\textbf{Church-Rosser}} &
481+\begin{array}{ll}
482+\mbox{If}\hg\Gamma\proves\vs\converts\vt \\
483+\mbox{then there is a common reduct $\vr$ such that}\:\\
484+\Gamma\proves\vs\reducesto\vr\hg\Gamma\proves\vt\reducesto\vr
485+\end{array}
486+\medskip
482487\\
483−\mbox{Subject Reduction}
488+\mbox{\textbf{Subject Reduction}} &
489+\begin{array}{ll}
490+\mbox{If} & \Gamma\proves\vs\Hab\vS\hg\Gamma\proves\vs\reduces\vt\\
491+\mbox{then}& \Gamma\proves\vt\Hab\vS
492+\end{array}
493+\medskip
484494\\
485−\mbox{Strengthening}
495+\mbox{\textbf{Cut}} &
496+\begin{array}{ll}
497+\mbox{If} & \Gamma_0,\LET\:\vx\defq\vs\Hab\vS,\Gamma_1\proves\vt\Hab\vT\\
498+\mbox{then} & \Gamma_0, \Gamma_1[\vs/\vx]\proves\vt[\vs/\vx]\Hab\vT[\vs/\vx]
499+\end{array}
500+\medskip
486501\\
487−\mbox{Cut}
502+\mbox{\textbf{Strengthening}} &
503+\begin{array}{ll}
504+\mbox{If} & \Gamma_0,\mathcal{B}(\vx, \vT),\Gamma_1\proves\vs\Hab\vS
505+\hg\vx\not\in\Gamma_1,\vs,\vS\\
506+\mbox{then} & \Gamma_0,\Gamma_1\proves\vs\Hab\vS\\
507+(\mbox{where} & \mathcal{B}(\vx, \vT) \proves \vx\Hab\vT)
508+\end{array}
488509\\
489−}
510+\end{array}
490511}
491512{Metatheoretic properties of \TT{}}
492513{metatheory}
493514
494−\TT{} respects the usual metatheoretic properties, as shown in Figure
495−\ref{metatheory}. Specifically: the \demph{Church-Rosser} property
496−(i.e. that distinct reduction sequences lead to the same normal form);
497−\demph{subject
498−reduction} (i.e. that computation preserves type); the \demph{cut} property
499−(i.e. that $\RW{let}$-bound terms may be substituted into their scope); and
500−\demph{strengthening} (i.e. that introducing new definitions into scope does
501−not affect typechecking).
515+We assume that \TT{} respects the usual metatheoretic properties, as shown in
516+Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property
517+(i.e. that distinct reduction sequences lead to the same normal form);
518+\demph{subject reduction} (i.e. that computation preserves type); the
519+\demph{cut} property (i.e. that $\RW{let}$-bound terms may be substituted into
520+their scope); and \demph{strengthening} (i.e. that removing unused definitions
521+from scope does not affect typechecking).
502522
503523One property which is noticeably absent is \demph{strong normalisation}.
504524Although desirable to preserve termination and decidability of type checking,