From 1928f46ad14670def752715addd36bc1543ebeff Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Tue, 10 Oct 2023 02:31:41 -0400
Subject: [PATCH] formalism: Give correctness metatheorem for typed hazelnut in
 relation to untyped

---
 formalism/typed.tex | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/formalism/typed.tex b/formalism/typed.tex
index 7a87922..7237066 100644
--- a/formalism/typed.tex
+++ b/formalism/typed.tex
@@ -1301,6 +1301,18 @@ \subsection{Metatheorems}
   \end{tikzcd}\]
 \end{theorem}
 
+\begin{theorem}[name=Correctness] \
+  \begin{enumerate}
+    \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
+      $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$ and
+      $\AUEAction{\erase{\ZCMV}}{\ZMV'}{\AMV}$, then $\equal{\erase{\ZCMV'}}{\ZMV'}$.
+
+    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
+      $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$ and
+      $\AUEAction{\erase{\ZCMV}}{\ZMV'}{\AMV}$, then $\equal{\erase{\ZCMV'}}{\ZMV'}$.
+  \end{enumerate}
+\end{theorem}
+
 \begin{theorem}[name=Sensibility] \
   \begin{enumerate}
     \item If $\zWellFormed{\ZCMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and