diff --git a/formalism/typed.tex b/formalism/typed.tex
index eadad7d..2f639bd 100644
--- a/formalism/typed.tex
+++ b/formalism/typed.tex
@@ -33,6 +33,7 @@ \subsection{Syntax}
            &       & \mid         & \ZCInconBrC{\ZCMV}{\ECMV}{\ECMV} \mid \ZCInconBrL{\ECMV}{\ZCMV}{\ECMV} \mid \ZCInconBrR{\ECMV}{\ECMV}{\ZCMV} \\
            &       & \mid         & \ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV} \mid \ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}
                      \mid           \ZCProjLSynNonMatchedProd{\ZCMV} \mid \ZCProjRSynNonMatchedProd{\ZCMV}
+
 \end{array}\]
 
 \subsubsection{Well-formedness}
@@ -213,6 +214,81 @@ \subsubsection{Well-formedness}
   }{
     \zWellFormed{\ZCInconType{\ZCMV}}
   }
+
+  \inferrule[WFLam3]{ }{
+    \zWellFormed{\ZLamInconAscT{x}{\ZTMV}{\ECMV}}
+  }
+
+  \inferrule[WFLam4]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZLamInconAscE{x}{\TMV}{\ZMV}}
+  }
+
+  \inferrule[WFLam5]{
+  }{
+    \zWellFormed{\ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}
+  }
+
+  \inferrule[WFLam6]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV}}
+  }
+
+  \inferrule[WFAp3]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZApSynNonMatchedArrowL{\ZMV}{\ECMV}}
+  }
+
+  \inferrule[WFAp4]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZApSynNonMatchedArrowR{\ECMV}{\ZMV}}
+  }
+
+  \inferrule[WFInconsistentBranches1]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[WFInconsistentBranches2]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}
+  }
+
+  \inferrule[WFInconsistentBranches3]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}
+  }
+
+  \inferrule[WFPair3]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZPairAnaNonMatchedProdL{\ZMV}{\ECMV}}
+  }
+
+  \inferrule[WFPair4]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZPairAnaNonMatchedProdR{\ECMV}{\ZMV}}
+  }
+
+  \inferrule[WFProjL2]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZProjLSynNonMatchedProd{\ZMV}}
+  }
+
+  \inferrule[WFProjR2]{
+    \zWellFormed{\ZMV}
+  }{
+    \zWellFormed{\ZProjRSynNonMatchedProd{\ZMV}}
+  }
 \end{mathpar}
 
 \subsection{Cursor erasure}
diff --git a/formalism/untyped.tex b/formalism/untyped.tex
index fe9b6d6..541203d 100644
--- a/formalism/untyped.tex
+++ b/formalism/untyped.tex
@@ -7,6 +7,14 @@
 
 \section{Untyped hazelnut}
 \label{sec:untyped}
+In this section we describe an \emph{untyped} version of the Hazelnut action calculus that might be
+layered with the marked lambda calculus to yield a structure editing calculus that supports
+non-local hole fixes.
+
+In comparison with the original calculus, this untyped version is not concerned at all with typing
+but only the manipulation of syntax. As such, the action judgments are simplified considerably; in
+particular, they are no longer bidirectional. The same core metatheorems, except sensibility which
+is no longer meaningful in this untyped context, still hold (see \cref{sec:untyped-metatheorems}).
 
 \begin{mechanization}
   \item hazelnut.agda
@@ -28,38 +36,38 @@ \subsection{Cursor erasure}
 
 \subsubsection{Type cursor erasure}
 \label{sec:untyped-type-cursor-erasure}
-\judgbox{\ensuremath{\cursorErase{\ZTMV}}} is a metafunction defined as follows:
+\judgbox{\ensuremath{\cursorErase{\ZTMV}}} is a metafunction $\ZTMName \to \TMName$ defined as follows:
 %
 \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}}
 \[\begin{array}{rcl}
   \cursorErasesToRow{\ZTCursor{\TMV}}{\TMV} \\
-  \cursorErasesToRow{(\ZTArrowL{\ZTMV}{\TMV})}{\TArrow{\cursorErase{\ZTMV}}{\TMV}} \\
-  \cursorErasesToRow{(\ZTArrowR{\TMV}{\ZTMV})}{\TArrow{\TMV}{\cursorErase{\ZTMV}}} \\
-  \cursorErasesToRow{(\ZTProdL{\ZTMV}{\TMV})}{\TProd{\cursorErase{\ZTMV}}{\TMV}} \\
-  \cursorErasesToRow{(\ZTProdR{\TMV}{\ZTMV})}{\TProd{\TMV}{\cursorErase{\ZTMV}}} \\
+  \cursorErasesToRow{(\ZTArrowL{\ZTMV}{\TMV})}{\TArrow{(\cursorErase{\ZTMV})}{\TMV}} \\
+  \cursorErasesToRow{(\ZTArrowR{\TMV}{\ZTMV})}{\TArrow{\TMV}{(\cursorErase{\ZTMV})}} \\
+  \cursorErasesToRow{(\ZTProdL{\ZTMV}{\TMV})}{\TProd{(\cursorErase{\ZTMV})}{\TMV}} \\
+  \cursorErasesToRow{(\ZTProdR{\TMV}{\ZTMV})}{\TProd{\TMV}{(\cursorErase{\ZTMV})}} \\
 \end{array}\]
 
 \subsubsection{Expression cursor erasure}
 \label{sec:untyped-expression-cursor-erasure}
-\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction defined as follows:
+\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction $\ZMName \to \EMName$ defined as follows:
 %
 \[\begin{array}{rcl}
   \cursorErasesToRow{\ZCursor{\EMV}}{\EMV} \\
-  \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\EMV})}{\ELam{x}{\cursorErase{\ZTMV}}{\EMV}} \\
-  \cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ELam{x}{\TMV}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZApL{\ZMV}{\EMV})}{\EAp{\cursorErase{\ZMV}}{\EMV}} \\
-  \cursorErasesToRow{(\ZApR{\EMV}{\ZMV})}{\EAp{\EMV}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZLetL{x}{\ZMV}{\EMV})}{\ELet{x}{\cursorErase{\ZMV}}{\EMV}} \\
-  \cursorErasesToRow{(\ZLetR{x}{\EMV}{\ZMV})}{\ELet{x}{\EMV}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZPlusL{\ZMV}{\EMV})}{\EPlus{\cursorErase{\ZMV}}{\EMV}} \\
-  \cursorErasesToRow{(\ZPlusR{\EMV}{\ZMV})}{\EPlus{\EMV}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZIfC{\ZMV}{\EMV_1}{\EMV_2})}{\EIf{\cursorErase{\ZMV}}{\EMV_1}{\EMV_2}} \\
-  \cursorErasesToRow{(\ZIfL{\EMV_1}{\ZMV}{\EMV_2})}{\EIf{\EMV_1}{\cursorErase{\ZMV}}{\EMV_2}} \\
-  \cursorErasesToRow{(\ZIfL{\EMV_1}{\EMV_2}{\ZMV})}{\EIf{\EMV_1}{\EMV_2}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZPairL{\ZMV}{\EMV})}{\EPair{\cursorErase{\ZMV}}{\EMV}} \\
-  \cursorErasesToRow{(\ZPairR{\EMV}{\ZMV})}{\EPair{\EMV}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZProjL{\ZMV})}{\EProjL{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZProjR{\ZMV})}{\EProjR{\cursorErase{\ZMV}}} \\
+  \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\EMV})}{\ELam{x}{(\cursorErase{\ZTMV})}{\EMV}} \\
+  \cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ELam{x}{\TMV}{(\cursorErase{\ZMV})}} \\
+  \cursorErasesToRow{(\ZApL{\ZMV}{\EMV})}{\EAp{(\cursorErase{\ZMV})}{\EMV}} \\
+  \cursorErasesToRow{(\ZApR{\EMV}{\ZMV})}{\EAp{\EMV}{(\cursorErase{\ZMV})}} \\
+  \cursorErasesToRow{(\ZLetL{x}{\ZMV}{\EMV})}{\ELet{x}{(\cursorErase{\ZMV})}{\EMV}} \\
+  \cursorErasesToRow{(\ZLetR{x}{\EMV}{\ZMV})}{\ELet{x}{\EMV}{(\cursorErase{\ZMV})}} \\
+  \cursorErasesToRow{(\ZPlusL{\ZMV}{\EMV})}{\EPlus{(\cursorErase{\ZMV})}{\EMV}} \\
+  \cursorErasesToRow{(\ZPlusR{\EMV}{\ZMV})}{\EPlus{\EMV}{(\cursorErase{\ZMV})}} \\
+  \cursorErasesToRow{(\ZIfC{\ZMV}{\EMV_1}{\EMV_2})}{\EIf{(\cursorErase{\ZMV})}{\EMV_1}{\EMV_2}} \\
+  \cursorErasesToRow{(\ZIfL{\EMV_1}{\ZMV}{\EMV_2})}{\EIf{\EMV_1}{(\cursorErase{\ZMV})}{\EMV_2}} \\
+  \cursorErasesToRow{(\ZIfL{\EMV_1}{\EMV_2}{\ZMV})}{\EIf{\EMV_1}{\EMV_2}{(\cursorErase{\ZMV})}} \\
+  \cursorErasesToRow{\ZPairL{\ZMV}{\EMV}}{\EPair{\cursorErase{\ZMV}}{\EMV}} \\
+  \cursorErasesToRow{\ZPairR{\EMV}{\ZMV}}{\EPair{\EMV}{\cursorErase{\ZMV}}} \\
+  \cursorErasesToRow{(\ZProjL{\ZMV})}{\EProjL{(\cursorErase{\ZMV})}} \\
+  \cursorErasesToRow{(\ZProjR{\ZMV})}{\EProjR{(\cursorErase{\ZMV})}} \\
 \end{array}\]
 
 \subsection{Action model}
@@ -586,13 +594,13 @@ \subsubsection{Expression actions}
   \inferrule[AEZipProjL]{
     \AUEAction{\ZMV}{\ZMV'}{\AMV}
   }{
-    \AUEAction{\ZProjL{\ZMV}{\EMV}}{\ZProjL{\ZMV'}{\EMV}}{\AMV}
+    \AUEAction{\ZProjL{\ZMV}}{\ZProjL{\ZMV'}}{\AMV}
   }
 
   \inferrule[AEZipProjR]{
     \AUEAction{\ZMV}{\ZMV'}{\AMV}
   }{
-    \AUEAction{\ZProjR{\EMV}{\ZMV}}{\ZProjR{\EMV}{\ZMV'}}{\AMV}
+    \AUEAction{\ZProjR{\ZMV}}{\ZProjR{\ZMV'}}{\AMV}
   }
 \end{mathparpagebreakable}
 
@@ -644,66 +652,80 @@ \subsubsection{Iterated actions}
 
 \subsection{Metatheorems}
 \label{sec:untyped-metatheorems}
-\begin{theorem}[name=Sensibility]
-\end{theorem}
 
 \begin{theorem}[name=Movement Erasure Invariance] \
   \begin{enumerate}
-    \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZTMV} =
-      \cursorErase{\ZTMV'}$.
+    \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$,
+      then $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$.
 
-    \item If $\AUEAction{\ZMV}{\ZMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZMV} =
-      \cursorErase{\ZMV'}$.
+    \item If $\AUEAction{\ZMV}{\ZMV'}{\AMove{\MMV}}$,
+      then $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$.
   \end{enumerate}
 \end{theorem}
 
 \begin{theorem}[name=Reachability] \
   \begin{enumerate}
-    \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$, then there exists $\AIMV$ such that
-      $\movements{\AIMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$.
-
-    \item If $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$, then there exists $\AIMV$ such that
-      $\movements{\AIMV}$ and $\AUEActionIter{\ZMV}{\ZMV'}{\AIMV}$.
+    \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$.
+
+    \item If $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUEActionIter{\ZMV}{\ZMV'}{\AIMV}$.
   \end{enumerate}
 \end{theorem}
 
 \begin{lemma}[name=Reach Up] \
   \begin{enumerate}
-    \item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
-      and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$.
-
-    \item If $\cursorErase{\ZMV} = \EMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
-      and $\AUEActionIter{\ZMV}{\ZTCursor{\EMV}}{\AIMV}$.
+    \item If $\cursorErase{\ZTMV} = \TMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$.
+
+    \item If $\cursorErase{\ZMV} = \EMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUEActionIter{\ZMV}{\ZTCursor{\EMV}}{\AIMV}$.
   \end{enumerate}
 \end{lemma}
 
 \begin{lemma}[name=Reach Down] \
   \begin{enumerate}
-    \item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
-      and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$.
-
-    \item If $\cursorErase{\ZMV} = \EMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
-      and $\AUEActionIter{\ZTCursor{\EMV}}{\ZMV}{\AIMV}$.
+    \item If $\cursorErase{\ZTMV} = \TMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$.
+
+    \item If $\cursorErase{\ZMV} = \EMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUEActionIter{\ZTCursor{\EMV}}{\ZMV}{\AIMV}$.
   \end{enumerate}
 \end{lemma}
 
 \begin{theorem}[name=Constructability] \
   \begin{enumerate}
-    \item For every $\TMV$, there exists $\AIMV$ such that
-      $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$.
+    \item For every $\TMV$,
+        there exists $\AIMV$
+          such that $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$.
 
-    \item For every $\EMV$, there exists $\AIMV$ such that
-      $\AUEActionIter{\ZCursor{\EEHole}}{\ZCursor{\EMV}}{\AIMV}$.
+    \item For every $\EMV$,
+        there exists $\AIMV$
+          such that $\AUEActionIter{\ZCursor{\EEHole}}{\ZCursor{\EMV}}{\AIMV}$.
   \end{enumerate}
 \end{theorem}
 
 \begin{theorem}[name=Determinism] \
   \begin{enumerate}
-    \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$, then
-      $\ZTMV' = \ZTMV''$.
+    \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$
+        and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$,
+      then $\ZTMV' = \ZTMV''$.
 
-    \item If $\AUEActionIter{\ZMV}{\ZMV'}{\AMV}$ and $\AUEActionIter{\ZMV}{\ZMV''}{\AMV}$, then
-      $\ZMV' = \ZMV''$.
+    \item If $\AUEActionIter{\ZMV}{\ZMV'}{\AMV}$
+        and $\AUEActionIter{\ZMV}{\ZMV''}{\AMV}$,
+      then $\ZMV' = \ZMV''$.
   \end{enumerate}
 \end{theorem}