diff --git a/formalism/preamble/preamble.tex b/formalism/preamble/preamble.tex
index 9420c87..e757a82 100644
--- a/formalism/preamble/preamble.tex
+++ b/formalism/preamble/preamble.tex
@@ -48,6 +48,9 @@
 \usepackage[dvipsnames]{xcolor}
 \usepackage[most]{tcolorbox}
 
+% diagrams
+\usepackage{quiver}
+
 % theorem types
 \declaretheorem[name=Theorem, parent=section]{theorem}
 \declaretheorem[name=Lemma, parent=theorem]{lemma}
diff --git a/formalism/quiver.sty b/formalism/quiver.sty
new file mode 100644
index 0000000..d1d7d07
--- /dev/null
+++ b/formalism/quiver.sty
@@ -0,0 +1,40 @@
+% *** quiver ***
+% A package for drawing commutative diagrams exported from https://q.uiver.app.
+%
+% This package is currently a wrapper around the `tikz-cd` package, importing necessary TikZ
+% libraries, and defining a new TikZ style for curves of a fixed height.
+%
+% Version: 1.3.0
+% Authors:
+% - varkor (https://github.com/varkor)
+% - AndréC (https://tex.stackexchange.com/users/138900/andr%C3%A9c)
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{quiver}[2021/01/11 quiver]
+
+% `tikz-cd` is necessary to draw commutative diagrams.
+\RequirePackage{tikz-cd}
+% `amssymb` is necessary for `\lrcorner` and `\ulcorner`.
+\RequirePackage{amssymb}
+% `calc` is necessary to draw curved arrows.
+\usetikzlibrary{calc}
+% `pathmorphing` is necessary to draw squiggly arrows.
+\usetikzlibrary{decorations.pathmorphing}
+
+% A TikZ style for curved arrows of a fixed height, due to AndréC.
+\tikzset{curve/.style={settings={#1},to path={(\tikztostart)
+    .. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
+    and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
+    .. (\tikztotarget)\tikztonodes}},
+    settings/.code={\tikzset{quiver/.cd,#1}
+        \def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}},
+    quiver/.cd,pos/.initial=0.35,height/.initial=0}
+
+% TikZ arrowhead/tail styles.
+\tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}}
+\tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}}
+\tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}}
+% TikZ arrow styles.
+\tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}}
+
+\endinput
diff --git a/formalism/symbols/typed.tex b/formalism/symbols/typed.tex
index f26b078..cadb681 100644
--- a/formalism/symbols/typed.tex
+++ b/formalism/symbols/typed.tex
@@ -1,5 +1,64 @@
 % !requires untyped
 
+%
+% marked zippered expressions
+%
+\newcommand{\ZCMName}{{\normalfont\textsf{ZMExp}}}
+\newcommand{\ZCMSet}{\ensuremath{\hat{E}}}
+\newcommand{\ZCMV}{\ensuremath{\underline{\check{e}}}}
+
+% cursor
+\definecolor{cursorhighlight}{RGB}{230,255,230}
+\definecolor{cursor}{RGB}{76,170,76}
+\newcommand{\ZCCursor}[1]{\ensuremath{\mathcolorbox{cursorhighlight}{\textcolor{cursor}{\bm{\triangleright}}#1\textcolor{cursor}{\bm{\triangleleft}}}}}
+
+% integers
+\newcommand{\ZCPlusL}[2]{\ensuremath{\ECPlus{#1}{#2}}}
+\newcommand{\ZCPlusR}[2]{\ensuremath{\ECPlus{#1}{#2}}}
+
+% lambdas
+\newcommand{\ZCLamT}[3]{\ensuremath{\ECLam{#1}{#2}{#3}}}
+\newcommand{\ZCLamE}[3]{\ensuremath{\ECLam{#1}{#2}{#3}}}
+\newcommand{\ZCApL}[2]{\ensuremath{\ECAp{#1}{#2}}}
+\newcommand{\ZCApR}[2]{\ensuremath{\ECAp{#1}{#2}}}
+
+% booleans
+\newcommand{\ZCIfC}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}}
+\newcommand{\ZCIfL}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}}
+\newcommand{\ZCIfR}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}}
+
+% let
+\newcommand{\ZCLetL}[3]{\ensuremath{\ECLet{#1}{#2}{#3}}}
+\newcommand{\ZCLetR}[3]{\ensuremath{\ECLet{#1}{#2}{#3}}}
+
+% pairs
+\newcommand{\ZCPairL}[2]{\ensuremath{\ECPair{#1}{#2}}}
+\newcommand{\ZCPairR}[2]{\ensuremath{\ECPair{#1}{#2}}}
+\newcommand{\ZCProjL}[1]{\ensuremath{\ECProjL{#1}}}
+\newcommand{\ZCProjR}[1]{\ensuremath{\ECProjR{#1}}}
+
+% errors
+\newcommand{\ZCInconType}[1]{\ensuremath{\ECInconType{#1}}}
+\newcommand{\ZCInconBrC}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}}
+\newcommand{\ZCInconBrL}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}}
+\newcommand{\ZCInconBrR}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}}
+\newcommand{\ZCInconAsc}[1]{\ensuremath{\ECInconAsc{#1}}}
+\newcommand{\ZCSynNonMatchedArrow}[1]{\ensuremath{\ECSynNonMatchedArrow{#1}}}
+\newcommand{\ZCSynNonMatchedProd}[1]{\ensuremath{\ECSynNonMatchedProd{#1}}}
+\newcommand{\ZCAnaNonMatchedArrow}[1]{\ensuremath{\ECAnaNonMatchedArrow{#1}}}
+\newcommand{\ZCAnaNonMatchedProd}[1]{\ensuremath{\ECAnaNonMatchedProd{#1}}}
+
+\newcommand{\ZCLamInconAscT}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}}
+\newcommand{\ZCLamInconAscE}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}}
+\newcommand{\ZCApSynNonMatchedArrowL}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}}
+\newcommand{\ZCApSynNonMatchedArrowR}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}}
+\newcommand{\ZCProjLSynNonMatchedProd}[1]{\ensuremath{\ECProjL{\ECSynNonMatchedProd{#1}}}}
+\newcommand{\ZCProjRSynNonMatchedProd}[1]{\ensuremath{\ECProjR{\ECSynNonMatchedProd{#1}}}}
+\newcommand{\ZCLamAnaNonMatchedArrowT}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}}
+\newcommand{\ZCLamAnaNonMatchedArrowE}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}}
+\newcommand{\ZCPairAnaNonMatchedProdL}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}}
+\newcommand{\ZCPairAnaNonMatchedProdR}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}}
+
 % zippered expression well-formedness
 \newcommand{\zWellFormed}[1]{\ensuremath{#1 ~{\normalfont\textsf{WF}}}}
 
diff --git a/formalism/typed.tex b/formalism/typed.tex
index 92854d3..bf59932 100644
--- a/formalism/typed.tex
+++ b/formalism/typed.tex
@@ -9,6 +9,10 @@
 
 \section{Typed hazelnut}
 \label{sec:typed}
+We now give a description of a \emph{typed} version of the Hazelnut action calculus that
+incorporates the marked lambda calculus to solve the problem of non-local hole fixes. Here, unlike
+in the integration of the untyped version and the marked lambda calculus given in
+\cref{sec:untyped}, remarking is performed only when necessary instead of after every action.
 
 \nomechanization{}
 
@@ -17,126 +21,197 @@ \subsection{Syntax}
 Zippered types are the same as in the untyped model.
 
 \[\begin{array}{rrcl}
-  \ZMName  & \ZMV  & \Coloneqq & \ZCursor{\ECMV} \mid \ZLamT{x}{\ZTMV}{\ECMV} \mid \ZLamE{x}{\TMV}{\ZMV} \mid \ZApL{\ZMV}{\ECMV} \mid \ZApR{\ECMV}{\ZMV} \\
-           &       & \mid         & \ZLetL{x}{\ZMV}{\ECMV} \mid \ZLetR{x}{\ECMV}{\ZMV} \\
-           &       & \mid         & \ZPlusL{\ZMV}{\ECMV} \mid \ZPlusR{\ECMV}{\ZMV} \\
-           &       & \mid         & \ZIfC{\ZMV}{\ECMV}{\ECMV} \mid \ZIfL{\ECMV}{\ZMV}{\ECMV} \mid \ZIfR{\ECMV}{\ECMV}{\ZMV} \\
-           &       & \mid         & \ZPairL{\ZMV}{\EMV} \mid \ZPairR{\EMV}{\ZMV} \mid \ZProjL{\ZMV} \mid \ZProjR{\ZMV} \\
-           &       & \mid         & \ZFree{x} \mid \ZInconType{\ZMV} \\
-           &       & \mid         & \ZLamInconAscT{x}{\ZTMV}{\ECMV} \mid \ZLamInconAscE{x}{\TMV}{\ZMV}
-                     \mid           \ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV} \mid \ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV}
-                     \mid           \ZApSynNonMatchedArrowL{\ZMV}{\ECMV} \mid \ZApSynNonMatchedArrowR{\ECMV}{\ZMV} \\
-           &       & \mid         & \ZInconBrC{\ZMV}{\ECMV}{\ECMV} \mid \ZInconBrL{\ECMV}{\ZMV}{\ECMV} \mid \ZInconBrR{\ECMV}{\ECMV}{\ZMV} \\
-           &       & \mid         & \ZPairAnaNonMatchedProdL{\ZMV}{\ECMV} \mid \ZPairAnaNonMatchedProdR{\ECMV}{\ZMV}
-                     \mid           \ZProjLSynNonMatchedProd{\ZMV} \mid \ZProjRSynNonMatchedProd{\ZMV}
+  \ZCMName & \ZCMV & \Coloneqq & \ZCCursor{\ECMV} \mid \ZCLamT{x}{\ZTMV}{\ECMV} \mid \ZCLamE{x}{\TMV}{\ZCMV} \mid \ZCApL{\ZCMV}{\ECMV} \mid \ZCApR{\ECMV}{\ZCMV} \\
+           &       & \mid         & \ZCLetL{x}{\ZCMV}{\ECMV} \mid \ZCLetR{x}{\ECMV}{\ZCMV} \\
+           &       & \mid         & \ZCPlusL{\ZCMV}{\ECMV} \mid \ZCPlusR{\ECMV}{\ZCMV} \\
+           &       & \mid         & \ZCIfC{\ZCMV}{\ECMV}{\ECMV} \mid \ZCIfL{\ECMV}{\ZCMV}{\ECMV} \mid \ZCIfR{\ECMV}{\ECMV}{\ZCMV} \\
+           &       & \mid         & \ZCPairL{\ZCMV}{\EMV} \mid \ZCPairR{\EMV}{\ZCMV} \mid \ZCProjL{\ZCMV} \mid \ZCProjR{\ZCMV} \\
+           &       & \mid         & \ZCInconType{\ZCMV} \\
+           &       & \mid         & \ZCLamInconAscT{x}{\ZTMV}{\ECMV} \mid \ZCLamInconAscE{x}{\TMV}{\ZCMV}
+                     \mid           \ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV} \mid \ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}
+                     \mid           \ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV} \mid \ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV} \\
+           &       & \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}
 \label{sec:typed-well-formedness}
-\judgbox{\ensuremath{\zWellFormed{\ZMV}}} $\ZMV$ is well-formed
+\judgbox{\ensuremath{\zWellFormed{\ZCMV}}} $\ZCMV$ is well-formed
 %
-\begin{mathpar}
+\begin{mathparpagebreakable}
   \inferrule[WFCursor]{ }{
-    \zWellFormed{\ZCursor{\ECMV}}
+    \zWellFormed{\ZCCursor{\ECMV}}
   }
 
   \inferrule[WFLam1]{ }{
-    \zWellFormed{\ZLamT{x}{\ZTMV}{\ECMV}}
+    \zWellFormed{\ZCLamT{x}{\ZTMV}{\ECMV}}
   }
 
   \inferrule[WFLam2]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZLamE{x}{\TMV}{\ZMV}}
+    \zWellFormed{\ZCLamE{x}{\TMV}{\ZCMV}}
+  }
+
+  \inferrule[WFLam3]{
+  }{
+    \zWellFormed{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}
+  }
+
+  \inferrule[WFLam4]{
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}}
+  }
+
+  \inferrule[WFLam5]{ }{
+    \zWellFormed{\ZCLamInconAscT{x}{\ZTMV}{\ECMV}}
+  }
+
+  \inferrule[WFLam6]{
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCLamInconAscE{x}{\TMV}{\ZCMV}}
   }
 
   \inferrule[WFAp1]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZApL{\ZMV}{\ECMV}}
+    \zWellFormed{\ZCApL{\ZCMV}{\ECMV}}
   }
 
   \inferrule[WFAp2]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCApR{\ECMV}{\ZCMV}}
+  }
+
+  \inferrule[WFAp3]{
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV}}
+  }
+
+  \inferrule[WFAp4]{
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZApR{\ECMV}{\ZMV}}
+    \zWellFormed{\ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV}}
   }
 
   \inferrule[WFLet1]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZLetL{x}{\ZMV}{\ECMV}}
+    \zWellFormed{\ZCLetL{x}{\ZCMV}{\ECMV}}
   }
 
   \inferrule[WFLet2]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZLetR{x}{\ECMV}{\ZMV}}
+    \zWellFormed{\ZCLetR{x}{\ECMV}{\ZCMV}}
   }
 
   \inferrule[WFPlus1]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZPlusL{\ZMV}{\ECMV}}
+    \zWellFormed{\ZCPlusL{\ZCMV}{\ECMV}}
   }
 
   \inferrule[WFPlus2]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZPlusR{\ECMV}{\ZMV}}
+    \zWellFormed{\ZCPlusR{\ECMV}{\ZCMV}}
   }
 
   \inferrule[WFIf1]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2}}
+    \zWellFormed{\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2}}
   }
 
   \inferrule[WFIf2]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2}}
+    \zWellFormed{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}
   }
 
   \inferrule[WFIf3]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV}}
+    \zWellFormed{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}
+  }
+
+  \inferrule[WFInconsistentBranches1]{
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[WFInconsistentBranches2]{
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}
+  }
+
+  \inferrule[WFInconsistentBranches3]{
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}
   }
 
   \inferrule[WFPair1]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZPairL{\ZMV}{\ECMV}}
+    \zWellFormed{\ZCPairL{\ZCMV}{\ECMV}}
   }
 
   \inferrule[WFPair2]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZPairR{\ECMV}{\ZMV}}
+    \zWellFormed{\ZCPairR{\ECMV}{\ZCMV}}
+  }
+
+  \inferrule[WFPair3]{
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}}
+  }
+
+  \inferrule[WFPair4]{
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}}
   }
 
   \inferrule[WFProjL1]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCProjL{\ZCMV}}
+  }
+
+  \inferrule[WFProjL2]{
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZProjL{\ZMV}}
+    \zWellFormed{\ZCProjLSynNonMatchedProd{\ZCMV}}
   }
 
   \inferrule[WFProjR1]{
-    \zWellFormed{\ZMV}
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZProjR{\ZMV}}
+    \zWellFormed{\ZCProjR{\ZCMV}}
   }
 
-  \inferrule[WFFree]{ }{
-    \zWellFormed{\ZFree{x}}
+  \inferrule[WFProjR2]{
+    \zWellFormed{\ZCMV}
+  }{
+    \zWellFormed{\ZCProjRSynNonMatchedProd{\ZCMV}}
   }
 
   \inferrule[WFInconsistentTypes]{
-    \notEqual{\ZMV}{\ZCursor{\ECMV}} \\
-    \zWellFormed{\ZMV}
+    \notEqual{\ZCMV}{\ZCCursor{\ECMV}} \\
+    \zWellFormed{\ZCMV}
   }{
-    \zWellFormed{\ZInconType{\ZMV}}
+    \zWellFormed{\ZCInconType{\ZCMV}}
   }
 
   \inferrule[WFLam3]{ }{
@@ -213,7 +288,7 @@ \subsubsection{Well-formedness}
   }{
     \zWellFormed{\ZProjRSynNonMatchedProd{\ZMV}}
   }
-\end{mathpar}
+\end{mathparpagebreakable}
 
 \subsection{Cursor erasure}
 \label{sec:typed-cursor-erasure}
@@ -224,26 +299,40 @@ \subsubsection{Type cursor erasure}
 
 \subsubsection{Expression cursor erasure}
 \label{sec:typed-expression-cursor-erasure}
-\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction defined as follows:
+\judgbox{\ensuremath{\cursorErase{\ZCMV}}} is a metafunction $\ZCMName \to \ECMName$ defined as follows:
 %
 \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}}
 \[\begin{array}{rcl}
-  \cursorErasesToRow{\ZCursor{\ECMV}}{\ECMV} \\
-  \cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\ECMV})}{\ECLam{x}{\cursorErase{\ZTMV}}{\ECMV}} \\
-  \cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ECLam{x}{\TMV}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZApL{\ZMV}{\ECMV})}{\ECAp{\cursorErase{\ZMV}}{\ECMV}} \\
-  \cursorErasesToRow{(\ZApR{\ECMV}{\ZMV})}{\ECAp{\ECMV}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZLetL{x}{\ZMV}{\ECMV})}{\ECLet{x}{\cursorErase{\ZMV}}{\ECMV}} \\
-  \cursorErasesToRow{(\ZLetR{x}{\ECMV}{\ZMV})}{\ECLet{x}{\ECMV}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZPlusL{\ZMV}{\ECMV})}{\ECPlus{\cursorErase{\ZMV}}{\ECMV}} \\
-  \cursorErasesToRow{(\ZPlusR{\ECMV}{\ZMV})}{\ECPlus{\ECMV}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{(\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2})}{\ECIf{\cursorErase{\ZMV}}{\ECMV_1}{\ECMV_2}} \\
-  \cursorErasesToRow{(\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2})}{\ECIf{\ECMV_1}{\cursorErase{\ZMV}}{\ECMV_2}} \\
-  \cursorErasesToRow{(\ZIfL{\ECMV_1}{\ECMV_2}{\ZMV})}{\ECIf{\ECMV_1}{\ECMV_2}{\cursorErase{\ZMV}}} \\
-  \cursorErasesToRow{\ZInconType{\ZMV}}{\cursorErase{\ZMV}} \\
-  \cursorErasesToRow{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}}{\ECIf{\cursorErase{\ZMV}}{\ECMV_1}{\ECMV_2}} \\
-  \cursorErasesToRow{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}{\ECIf{\ECMV_1}{\cursorErase{\ZMV}}{\ECMV_2}} \\
-  \cursorErasesToRow{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}{\ECIf{\ECMV_1}{\ECMV_2}{\cursorErase{\ZMV}}} \\
+  \cursorErasesToRow{\ZCCursor{\ECMV}}{\ECMV} \\
+  \cursorErasesToRow{(\ZCLamT{x}{\ZTMV}{\ECMV})}{\ECLam{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\
+  \cursorErasesToRow{(\ZCLamE{x}{\TMV}{\ZCMV})}{\ECLam{x}{\TMV}{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\
+  \cursorErasesToRow{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{\ZCLamInconAscT{x}{\ZTMV}{\ECMV}}{\ECLamInconAsc{x}{(\cursorErase{\ZTMV})}{\ECMV}} \\
+  \cursorErasesToRow{\ZCLamInconAscE{x}{\TMV}{\ZCMV}}{\ECLamInconAsc{x}{\TMV}{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{(\ZCApL{\ZCMV}{\ECMV})}{\ECAp{(\cursorErase{\ZCMV})}{\ECMV}} \\
+  \cursorErasesToRow{(\ZCApR{\ECMV}{\ZCMV})}{\ECAp{\ECMV}{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{(\ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV})}{\ECApSynNonMatchedArrow{\cursorErase{\ZCMV}}{\ECMV}} \\
+  \cursorErasesToRow{(\ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV})}{\ECApSynNonMatchedArrow{\ECMV}{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{(\ZCLetL{x}{\ZCMV}{\ECMV})}{\ECLet{x}{(\cursorErase{\ZCMV})}{\ECMV}} \\
+  \cursorErasesToRow{(\ZCLetR{x}{\ECMV}{\ZCMV})}{\ECLet{x}{\ECMV}{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{(\ZCPlusL{\ZCMV}{\ECMV})}{\ECPlus{(\cursorErase{\ZCMV})}{\ECMV}} \\
+  \cursorErasesToRow{(\ZCPlusR{\ECMV}{\ZCMV})}{\ECPlus{\ECMV}{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{(\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2})}{\ECIf{(\cursorErase{\ZCMV})}{\ECMV_1}{\ECMV_2}} \\
+  \cursorErasesToRow{(\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2})}{\ECIf{\ECMV_1}{(\cursorErase{\ZCMV})}{\ECMV_2}} \\
+  \cursorErasesToRow{(\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV})}{\ECIf{\ECMV_1}{\ECMV_2}{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\ECInconBr{(\cursorErase{\ZCMV})}{\ECMV_1}{\ECMV_2}} \\
+  \cursorErasesToRow{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\ECInconBr{\ECMV_1}{(\cursorErase{\ZCMV})}{\ECMV_2}} \\
+  \cursorErasesToRow{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\ECInconBr{\ECMV_1}{\ECMV_2}{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{\ZCPairL{\ZCMV}{\ECMV}}{\ECPair{\cursorErase{\ZCMV}}{\ECMV}} \\
+  \cursorErasesToRow{\ZCPairR{\ECMV}{\ZCMV}}{\ECPair{\ECMV}{\cursorErase{\ZCMV}}} \\
+  \cursorErasesToRow{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}}{\ECPairAnaNonMatchedProd{\cursorErase{\ZCMV}}{\ECMV}} \\
+  \cursorErasesToRow{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}}{\ECPairAnaNonMatchedProd{\ECMV}{\cursorErase{\ZCMV}}} \\
+  \cursorErasesToRow{(\ZCProjL{\ZCMV})}{\ECProjL{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{(\ZCProjLSynNonMatchedProd{\ZCMV})}{\ECProjLSynNonMatchedProd{\cursorErase{\ZCMV}}} \\
+  \cursorErasesToRow{(\ZCProjR{\ZCMV})}{\ECProjR{(\cursorErase{\ZCMV})}} \\
+  \cursorErasesToRow{(\ZCProjRSynNonMatchedProd{\ZCMV})}{\ECProjRSynNonMatchedProd{\cursorErase{\ZCMV}}} \\
+  \cursorErasesToRow{\ZCInconType{\ZCMV}}{\ECInconType{\cursorErase{\ZCMV}}} \\
 \end{array}\]
 
 \subsection{Action model}
@@ -260,144 +349,256 @@ \subsubsection{Type actions}
 
 \subsubsection{Expression movement}
 \label{sec:typed-expression-movement}
-\judgbox{\ensuremath{\AUEMove{\ZMV}{\ZMV'}{\MMV}}}
+\judgbox{\ensuremath{\AUEMove{\ZCMV}{\ZCMV'}{\MMV}}}
 %
 \begin{mathparpagebreakable}
   \inferrule[AEMLamChild1]{ }{
-    \ASEMChild{\ECLam{x}{\TMV}{\ECMV}}{\ZLamT{x}{\ZTCursor{\TMV}}{\ECMV}}{1}
+    \ASEMChild{\ECLam{x}{\TMV}{\ECMV}}{\ZCLamT{x}{\ZTCursor{\TMV}}{\ECMV}}{1}
   }
 
   \inferrule[AEMLamChild2]{ }{
-    \ASEMChild{\ECLam{x}{\TMV}{\ECMV}}{\ZLamE{x}{\TMV}{\ZCursor{\ECMV}}}{2}
+    \ASEMChild{\ECLam{x}{\TMV}{\ECMV}}{\ZCLamE{x}{\TMV}{\ZCCursor{\ECMV}}}{2}
+  }
+
+  \inferrule[AEMLamChild3]{ }{
+    \ASEMChild{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TMV}}{\ECMV}}{1}
+  }
+
+  \inferrule[AEMLamChild4]{ }{
+    \ASEMChild{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCCursor{\ECMV}}}{2}
+  }
+
+  \inferrule[AEMLamChild5]{ }{
+    \ASEMChild{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\ZCLamInconAscT{x}{\ZTCursor{\TMV}}{\ECMV}}{1}
+  }
+
+  \inferrule[AEMLamChild6]{ }{
+    \ASEMChild{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\ZCLamInconAscE{x}{\TMV}{\ZCCursor{\ECMV}}}{2}
   }
 
   \inferrule[AEMLamParent1]{ }{
-    \ASEMParent{\ZLamT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLam{x}{\TMV}{\ECMV}}
+    \ASEMParent{\ZCLamT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLam{x}{\TMV}{\ECMV}}
   }
 
   \inferrule[AEMLamParent2]{ }{
-    \ASEMParent{\ZLamE{x}{\TMV}{\ZCursor{\ECMV}}}{\ECLam{x}{\TMV}{\ECMV}}
+    \ASEMParent{\ZCLamE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLam{x}{\TMV}{\ECMV}}
+  }
+
+  \inferrule[AEMLamParent3]{ }{
+    \ASEMParent{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}
+  }
+
+  \inferrule[AEMLamParent4]{ }{
+    \ASEMParent{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}
+  }
+
+  \inferrule[AEMLamParent5]{ }{
+    \ASEMParent{\ZCLamInconAscT{x}{\ZTCursor{\TMV}}{\ECMV}}{\ECLamInconAsc{x}{\TMV}{\ECMV}}
+  }
+
+  \inferrule[AEMLamParent6]{ }{
+    \ASEMParent{\ZCLamInconAscE{x}{\TMV}{\ZCCursor{\ECMV}}}{\ECLamInconAsc{x}{\TMV}{\ECMV}}
   }
 
   \inferrule[AEMApChild1]{ }{
-    \ASEMChild{\ECAp{\ECMV_1}{\ECMV_2}}{\ZApL{\ZCursor{\ECMV_1}}{\ECMV_2}}{1}
+    \ASEMChild{\ECAp{\ECMV_1}{\ECMV_2}}{\ZCApL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1}
   }
 
   \inferrule[AEMApChild2]{ }{
-    \ASEMChild{\ECAp{\ECMV_1}{\ECMV_2}}{\ZApR{\ECMV_1}{\ZCursor{\ECMV_2}}}{2}
+    \ASEMChild{\ECAp{\ECMV_1}{\ECMV_2}}{\ZCApR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2}
+  }
+
+  \inferrule[AEMApChild3]{ }{
+    \ASEMChild{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}{\ZCApSynNonMatchedArrowL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1}
+  }
+
+  \inferrule[AEMApChild4]{ }{
+    \ASEMChild{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2}
   }
 
   \inferrule[AEMApParent1]{ }{
-    \ASEMParent{\ZApL{\ZCursor{\ECMV_1}}{\ECMV_2}}{\ECAp{\ECMV_1}{\ECMV_2}}
+    \ASEMParent{\ZCApL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECAp{\ECMV_1}{\ECMV_2}}
   }
 
   \inferrule[AEMApParent2]{ }{
-    \ASEMParent{\ZApR{\ECMV_1}{\ZCursor{\ECMV_2}}}{\ECAp{\ECMV_1}{\ECMV_2}}
+    \ASEMParent{\ZCApR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECAp{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[AEMApParent3]{ }{
+    \ASEMParent{\ZCApSynNonMatchedArrowL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[AEMApParent4]{ }{
+    \ASEMParent{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}
   }
 
   \inferrule[AEMLetChild1]{ }{
-    \ASEMChild{\ECLet{x}{\ECMV_1}{\ECMV_2}}{\ZLetL{x}{\ZCursor{\ECMV_1}}{\ECMV_2}}{1}
+    \ASEMChild{\ECLet{x}{\ECMV_1}{\ECMV_2}}{\ZCLetL{x}{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1}
   }
 
   \inferrule[AEMLetChild2]{ }{
-    \ASEMChild{\ECLet{x}{\ECMV_1}{\ECMV_2}}{\ZLetR{x}{\ECMV_1}{\ZCursor{\ECMV_2}}}{2}
+    \ASEMChild{\ECLet{x}{\ECMV_1}{\ECMV_2}}{\ZCLetR{x}{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2}
   }
 
   \inferrule[AEMLetParent1]{ }{
-    \ASEMParent{\ZLetL{x}{\ZCursor{\ECMV_1}}{\ECMV_2}}{\ECLet{x}{\ECMV_1}{\ECMV_2}}
+    \ASEMParent{\ZCLetL{x}{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECLet{x}{\ECMV_1}{\ECMV_2}}
   }
 
   \inferrule[AEMLetParent2]{ }{
-    \ASEMParent{\ZLetR{x}{\ECMV_1}{\ZCursor{\ECMV_2}}}{\ECLet{x}{\ECMV_1}{\ECMV_2}}
+    \ASEMParent{\ZCLetR{x}{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECLet{x}{\ECMV_1}{\ECMV_2}}
   }
 
   \inferrule[AEMPlusChild1]{ }{
-    \ASEMChild{\ECPlus{\ECMV_1}{\ECMV_2}}{\ZPlusL{\ZCursor{\ECMV_1}}{\ECMV_2}}{1}
+    \ASEMChild{\ECPlus{\ECMV_1}{\ECMV_2}}{\ZCPlusL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1}
   }
 
   \inferrule[AEMPlusChild2]{ }{
-    \ASEMChild{\ECPlus{\ECMV_1}{\ECMV_2}}{\ZPlusR{\ECMV_1}{\ZCursor{\ECMV_2}}}{2}
+    \ASEMChild{\ECPlus{\ECMV_1}{\ECMV_2}}{\ZCPlusR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2}
   }
 
   \inferrule[AEMPlusParent1]{ }{
-    \ASEMParent{\ZPlusL{\ZCursor{\ECMV_1}}{\ECMV_2}}{\ECPlus{\ECMV_1}{\ECMV_2}}
+    \ASEMParent{\ZCPlusL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECPlus{\ECMV_1}{\ECMV_2}}
   }
 
   \inferrule[AEMPlusParent2]{ }{
-    \ASEMParent{\ZPlusR{\ECMV_1}{\ZCursor{\ECMV_2}}}{\ECPlus{\ECMV_1}{\ECMV_2}}
+    \ASEMParent{\ZCPlusR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECPlus{\ECMV_1}{\ECMV_2}}
   }
 
   \inferrule[AEMIfChild1]{ }{
-    \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZIfC{\ZCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{1}
+    \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCIfC{\ZCCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{1}
   }
 
   \inferrule[AEMIfChild2]{ }{
-    \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZIfL{\ECMV_1}{\ZCursor{\ECMV_2}}{\ECMV_3}}{2}
+    \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCIfL{\ECMV_1}{\ZCCursor{\ECMV_2}}{\ECMV_3}}{2}
   }
 
   \inferrule[AEMIfChild3]{ }{
-    \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZCursor{\ECMV_3}}}{3}
+    \ASEMChild{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{3}
   }
 
   \inferrule[AEMIfParent1]{ }{
-    \ASEMParent{\ZIfC{\ZCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
+    \ASEMParent{\ZCIfC{\ZCCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
   }
 
   \inferrule[AEMIfParent2]{ }{
-    \ASEMParent{\ZIfL{\ECMV_1}{\ZCursor{\ECMV_2}}{\ECMV_3}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
+    \ASEMParent{\ZCIfL{\ECMV_1}{\ZCCursor{\ECMV_2}}{\ECMV_3}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
   }
 
   \inferrule[AEMIfParent3]{ }{
-    \ASEMParent{\ZIfR{\ECMV_1}{\ECMV_2}{\ZCursor{\ECMV_3}}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
-  }
-
-  \inferrule[AEMInconsistentTypesChild]{
-    \ASEMChild{\ZMV}{\ZMV'}{\MChildNMV}
-  }{
-    \ASEMChild{\ZInconType{\ZMV}}{\ZInconType{\ZMV'}}{\MChildNMV}
-  }
-
-  \inferrule[AEMInconsistentTypesParent]{
-    \ASEMParent{\ZMV}{\ZMV'}
-  }{
-    \ASEMParent{\ZInconType{\ZMV}}{\ZInconType{\ZMV'}}
+    \ASEMParent{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
   }
 
   \inferrule[AEMInconsistentBranchesChild1]{ }{
-    \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZInconBrC{\ZCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{1}
+    \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCInconBrC{\ZCCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{1}
   }
 
   \inferrule[AEMInconsistentBranchesChild2]{ }{
-    \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZInconBrL{\ECMV_1}{\ZCursor{\ECMV_2}}{\ECMV_3}}{2}
+    \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCInconBrL{\ECMV_1}{\ZCCursor{\ECMV_2}}{\ECMV_3}}{2}
   }
 
   \inferrule[AEMInconsistentBranchesChild3]{ }{
-    \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZCursor{\ECMV_3}}}{3}
+    \ASEMChild{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{3}
   }
 
   \inferrule[AEMInconsistentBranchesParent1]{ }{
-    \ASEMParent{\ZInconBrC{\ZCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}
+    \ASEMParent{\ZCInconBrC{\ZCCursor{\ECMV_1}}{\ECMV_2}{\ECMV_3}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}
   }
 
   \inferrule[AEMInconsistentBranchesParent2]{ }{
-    \ASEMParent{\ZInconBrC{\ECMV_1}{\ZCursor{\ECMV_2}}{\ECMV_3}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}
+    \ASEMParent{\ZCInconBrC{\ECMV_1}{\ZCCursor{\ECMV_2}}{\ECMV_3}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}
   }
 
   \inferrule[AEMInconsistentBranchesParent3]{ }{
-    \ASEMParent{\ZInconBrC{\ECMV_1}{\ECMV_2}{\ZCursor{\ECMV_3}}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}
+    \ASEMParent{\ZCInconBrC{\ECMV_1}{\ECMV_2}{\ZCCursor{\ECMV_3}}}{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}
+  }
+
+  \inferrule[AEMPairChild1]{ }{
+    \ASEMChild{\ECPair{\ECMV_1}{\ECMV_2}}{\ZCPairL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1}
+  }
+
+  \inferrule[AEMPairChild2]{ }{
+    \ASEMChild{\ECPair{\ECMV_1}{\ECMV_2}}{\ZCPairR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2}
+  }
+
+  \inferrule[AEMPairChild3]{ }{
+    \ASEMChild{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}{\ZCPairAnaNonMatchedProdL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{1}
+  }
+
+  \inferrule[AEMPairChild4]{ }{
+    \ASEMChild{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}{\ZCPairAnaNonMatchedProdR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{2}
+  }
+
+  \inferrule[AEMPairParent1]{ }{
+    \ASEMParent{\ZCPairL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECPair{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[AEMPairParent2]{ }{
+    \ASEMParent{\ZCPairR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECPair{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[AEMPairParent3]{ }{
+    \ASEMParent{\ZCPairAnaNonMatchedProdL{\ZCCursor{\ECMV_1}}{\ECMV_2}}{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[AEMPairParent4]{ }{
+    \ASEMParent{\ZCPairAnaNonMatchedProdR{\ECMV_1}{\ZCCursor{\ECMV_2}}}{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[AEMProjLChild1]{ }{
+    \ASEMChild{\ECProjL{\ECMV}}{\ZCProjL{\ZCCursor{\ECMV}}}{1}
+  }
+
+  \inferrule[AEMProjLChild2]{ }{
+    \ASEMChild{\ECProjLSynNonMatchedProd{\ECMV}}{\ZCProjLSynNonMatchedProd{\ZCCursor{\ECMV}}}{1}
+  }
+
+  \inferrule[AEMProjLParent1]{ }{
+    \ASEMParent{\ZCProjL{\ZCCursor{\ECMV}}}{\ECProjL{\ECMV}}
+  }
+
+  \inferrule[AEMProjLParent2]{ }{
+    \ASEMParent{\ZCProjLSynNonMatchedProd{\ZCCursor{\ECMV}}}{\ECProjLSynNonMatchedProd{\ECMV}}
+  }
+
+  \inferrule[AEMProjRChild1]{ }{
+    \ASEMChild{\ECProjR{\ECMV}}{\ZCProjR{\ZCCursor{\ECMV}}}{1}
+  }
+
+  \inferrule[AEMProjRChild2]{ }{
+    \ASEMChild{\ECProjRSynNonMatchedProd{\ECMV}}{\ZCProjRSynNonMatchedProd{\ZCCursor{\ECMV}}}{1}
+  }
+
+  \inferrule[AEMProjRParent1]{ }{
+    \ASEMParent{\ZCProjR{\ZCCursor{\ECMV}}}{\ECProjR{\ECMV}}
+  }
+
+  \inferrule[AEMProjRParent2]{ }{
+    \ASEMParent{\ZCProjRSynNonMatchedProd{\ZCCursor{\ECMV}}}{\ECProjRSynNonMatchedProd{\ECMV}}
+  }
+
+  \inferrule[AEMInconsistentTypesChild]{
+    \ASEMChild{\ZCMV}{\ZCMV'}{\MChildNMV}
+  }{
+    \ASEMChild{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}{\MChildNMV}
+  }
+
+  \inferrule[AEMInconsistentTypesParent]{
+    \ASEMParent{\ZCMV}{\ZCMV'}
+  }{
+    \ASEMParent{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}
   }
 \end{mathparpagebreakable}
 
 \subsubsection{Synthetic expression actions}
 \label{sec:typed-synthetic-expression-actions}
-\judgbox{\ensuremath{\ASAction{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AMV}}}
+\judgbox{\ensuremath{\ASAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}}}
 
 \paragraph{Movement}
 \begin{mathpar}
   \inferrule[ASEMove]{
-    \ASEMove{\ZMV}{\ZMV'}{\MMV}
+    \ASEMove{\ZCMV}{\ZCMV'}{\MMV}
   }{
-    \ASMove{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV}{\MMV}
+    \ASMove{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV}{\MMV}
   }
 \end{mathpar}
 
@@ -413,93 +614,109 @@ \subsubsection{Synthetic expression actions}
   \inferrule[ASEConVar]{
     \inCtx{\ctx}{x}{\TMV}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECEHole}}{\TUnknown}{\ZCursor{x}}{\TMV}{\SVar{x}}
+    \ASCon{\ctx}{\ZCCursor{\ECEHole}}{\TUnknown}{\ZCCursor{x}}{\TMV}{\SVar{x}}
   }
 
   \inferrule[ASEConFree]{
     \notInCtx{\ctx}{x}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECEHole}}{\TUnknown}{\ZCursor{\ZFree{x}}}{\TUnknown}{\SVar{x}}
+    \ASCon{\ctx}{\ZCCursor{\ECEHole}}{\TUnknown}{\ZCCursor{\ECFree{x}}}{\TUnknown}{\SVar{x}}
   }
 
   \inferrule[ASEConLam]{
     \ctxSynFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TMV'}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}{\TArrow{\TUnknown}{\TMV'}}{\SLam{x}}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}{\TArrow{\TUnknown}{\TMV'}}{\SLam{x}}
   }
 
   \inferrule[ASEConApL1]{
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZApL{\ECInconType{\ECMV}}{\ZCursor{\ECEHole}}}{\TMV_2}{\SApL}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApL{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}}{\TMV_2}{\SApL}
   }
 
   \inferrule[ASEConApL2]{
     \notMatchedArrow{\TMV}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZApL{\ECInconType{\ECMV}}{\ZCursor{\ECEHole}}}{\TUnknown}{\SApL}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApL{\ECInconType{\ECMV}}{\ZCCursor{\ECEHole}}}{\TUnknown}{\SApL}
   }
 
-  \inferrule[ASEConApR]{ }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZApR{\ZCursor{\ECEHole}}{\ECMV}}{\TUnknown}{\SApR}
+  \inferrule[ASEConApR]{
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
+  }{
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCApR{\ZCCursor{\ECEHole}}{\ECMV'}}{\TUnknown}{\SApR}
   }
 
   \inferrule[ASEConLet1]{ }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZLetL{x}{\ECMV}{\ZCursor{\ECEHole}}}{\TUnknown}{\SLetL{x}}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCLetL{x}{\ECMV}{\ZCCursor{\ECEHole}}}{\TUnknown}{\SLetL{x}}
   }
 
   \inferrule[ASEConLet2]{
     \ctxSynFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TMV'}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZLetR{x}{\ZCursor{\ECEHole}}{\ECMV'}}{\TMV'}{\SLetL{x}}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCLetR{x}{\ZCCursor{\ECEHole}}{\ECMV'}}{\TMV'}{\SLetL{x}}
   }
 
   \inferrule[ASEConNum]{ }{
-    \ASCon{\ctx}{\ZCursor{\ECEHole}}{\TUnknown}{\ZCursor{\ENumMV}}{\TNum}{\SLit{\ENumMV}}
+    \ASCon{\ctx}{\ZCCursor{\ECEHole}}{\TUnknown}{\ZCCursor{\ENumMV}}{\TNum}{\SLit{\ENumMV}}
   }
 
-  \inferrule[ASEConPlusL1]{
-    \consistent{\TMV}{\TNum}
+  \inferrule[ASEConPlusL]{
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TNum}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZPlusR{\ECMV}{\ZCursor{\ECEHole}}}{\TNum}{\SPlusL}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusR{\ECMV'}{\ZCCursor{\ECEHole}}}{\TNum}{\SPlusL}
   }
 
-  \inferrule[ASEConPlusL2]{
-    \inconsistent{\TMV}{\TNum}
+  \inferrule[ASEConPlusR]{
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TNum}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZPlusR{\ECInconType{\ECMV}}{\ZCursor{\ECEHole}}}{\TNum}{\SPlusL}
-  } \\
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPlusL{\ZCCursor{\ECEHole}}{\ECMV'}}{\TNum}{\SPlusR}
+  }
 
-  \inferrule[ASEConPlusR1]{
-    \consistent{\TMV}{\TNum}
+  \inferrule[ASEConIfC]{
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TBool}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZPlusL{\ZCursor{\ECEHole}}{\ECMV}}{\TNum}{\SPlusR}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfL{\ECMV'}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC}
   }
 
-  \inferrule[ASEConPlusR2]{
-    \inconsistent{\TMV}{\TNum}
-  }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZPlusL{\ZCursor{\ECEHole}}{\ECInconType{\ECMV}}}{\TNum}{\SPlusR}
+  \inferrule[ASEConIfL]{ }{
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECMV}{\ECEHole}}{\TMV}{\SIfL}
+  }
+
+  \inferrule[ASEConIfR]{ }{
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECEHole}{\ECMV}}{\TMV}{\SIfR}
+  }
+
+  \inferrule[ASEConPairL]{ }{
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPairL{\ZCCursor{\ECMV}}{\ECEHole}}{\TProd{\TMV}{\TUnknown}}{\SPairL}
+  }
+
+  \inferrule[ASEConPairR]{ }{
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCPairR{\ECEHole}{\ZCCursor{\ECMV}}}{\TProd{\TUnknown}{\TMV}}{\SPairR}
   }
 
-  \inferrule[ASEConIfC1]{
-    \consistent{\TMV}{\TBool}
+  \inferrule[ASEConProjL]{
+    \matchedProd{\TMV}{\TMV_1}{\TMV_2}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZIfL{\ECMV}{\ZCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCProjL{\ZCCursor{\ECMV}}}{\TMV_1}{\SProjL}
   }
 
-  \inferrule[ASEConIfC2]{
-    \inconsistent{\TMV}{\TBool}
+  \inferrule[ASEConProjL2]{
+    \notMatchedProd{\TMV}
   }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZIfL{\ECInconType{\ECMV}}{\ZCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC}
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCProjLSynNonMatchedProd{\ZCCursor{\ECMV}}}{\TUnknown}{\SProjL}
   }
 
-  \inferrule[ASEConIfL]{ }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZIfC{\ZCursor{\ECEHole}}{\ECMV}{\ECEHole}}{\TMV}{\SIfL}
+  \inferrule[ASEConProjR1]{
+    \matchedProd{\TMV}{\TMV_1}{\TMV_2}
+  }{
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCProjR{\ZCCursor{\ECMV}}}{\TMV_2}{\SProjR}
   }
 
-  \inferrule[ASEConIfR]{ }{
-    \ASCon{\ctx}{\ZCursor{\ECMV}}{\TMV}{\ZIfC{\ZCursor{\ECEHole}}{\ECEHole}{\ECMV}}{\TMV}{\SIfR}
+  \inferrule[ASEConProjR2]{
+    \notMatchedProd{\TMV}
+  }{
+    \ASCon{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCProjRSynNonMatchedProd{\ZCCursor{\ECMV}}}{\TUnknown}{\SProjR}
   }
 \end{mathparpagebreakable}
 
@@ -509,7 +726,7 @@ \subsubsection{Synthetic expression actions}
     \AUTAction{\ZTMV_1}{\ZTMV_1'}{\AMV} \\
     \equal{\cursorErase{\ZTMV_1}}{\cursorErase{\ZTMV_1'}}
   }{
-    \ASEAction{\ctx}{\ZLamT{x}{\ZTMV_1}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\ZLamT{x}{\ZTMV_1'}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\AMV}
+    \ASEAction{\ctx}{\ZCLamT{x}{\ZTMV_1}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\ZCLamT{x}{\ZTMV_1'}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\AMV}
   }
 
   \inferrule[ASEZipLamT2]{
@@ -517,242 +734,320 @@ \subsubsection{Synthetic expression actions}
     \notEqual{\cursorErase{\ZTMV_1}}{\cursorErase{\ZTMV_1'}} \\
     \ctxSynFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_1'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2'}
   }{
-    \ASEAction{\ctx}{\ZLamT{x}{\ZTMV_1}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\ZLamT{x}{\ZTMV_1'}{\ECMV'}}{\TArrow{\cursorErase{\ZTMV_1'}}{\TMV_2'}}{\AMV}
+    \ASEAction{\ctx}{\ZCLamT{x}{\ZTMV_1}{\ECMV}}{\TArrow{\cursorErase{\ZTMV_1}}{\TMV_2}}{\ZCLamT{x}{\ZTMV_1'}{\ECMV'}}{\TArrow{\cursorErase{\ZTMV_1'}}{\TMV_2'}}{\AMV}
   }
 
   \inferrule[ASEZipLamE]{
-    \ASEAction{\extendCtx{\ctx}{x}{\TMV_1}}{\ZMV}{\TMV_2}{\ZMV'}{\TMV_2'}{\AMV}
+    \ASEAction{\extendCtx{\ctx}{x}{\TMV_1}}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV}
   }{
-    \ASEAction{\ctx}{\ZLamE{x}{\TMV_1}{\ZMV}}{\TArrow{\TMV_1}{\TMV_2}}{\ZLamE{x}{\TMV_1}{\ZMV'}}{\TArrow{\ZTMV_1}{\TMV_2'}}{\AMV}
+    \ASEAction{\ctx}{\ZCLamE{x}{\TMV_1}{\ZCMV}}{\TArrow{\TMV_1}{\TMV_2}}{\ZCLamE{x}{\TMV_1}{\ZCMV'}}{\TArrow{\ZTMV_1}{\TMV_2'}}{\AMV}
   }
 
   \inferrule[ASEZipApL1]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\
+    \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\
     \matchedArrow{\TMV_1'}{\TMV_2}{\TMV_3} \\
     \ctxAnaType{\ctx}{\ECMV_2}{\TMV_2}
   }{
-    \ASEAction{\ctx}{\ZApL{\ZMV_1}{\ECMV_2}}{\TMV}{\ZApL{\ZMV_1'}{\ECMV_2}}{\TMV_3}{\AMV}
+    \ASEAction{\ctx}{\ZCApL{\ZCMV_1}{\ECMV_2}}{\TMV}{\ZCApL{\ZCMV_1'}{\ECMV_2}}{\TMV_3}{\AMV}
   }
 
   \inferrule[ASEZipApL2]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\
+    \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\
     \matchedArrow{\TMV_1'}{\TMV_2}{\TMV_3} \\
     \ctxNotAnaType{\ctx}{\ECMV_2}{\TMV_2}
   }{
-    \ASEAction{\ctx}{\ZApL{\ZMV_1}{\ECMV_2}}{\TMV}{\ZApL{\ZMV_1'}{\ECInconType{\ECMV_2}}}{\TMV_3}{\AMV}
+    \ASEAction{\ctx}{\ZCApL{\ZCMV_1}{\ECMV_2}}{\TMV}{\ZCApL{\ZCMV_1'}{\ECInconType{\ECMV_2}}}{\TMV_3}{\AMV}
   }
 
   \inferrule[ASEZipApL3]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\\\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\
+    \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\
     \notMatchedArrow{\TMV_1'}
   }{
-    \ASEAction{\ctx}{\ZApL{\ZMV_1}{\ECMV_2}}{\TMV}{\ZApL{\ECInconType{\ZMV_1'}}{\ECMV_2}}{\TUnknown}{\AMV}
+    \ASEAction{\ctx}{\ZCApL{\ZCMV_1}{\ECMV_2}}{\TMV}{\ZCApSynNonMatchedArrowL{\ZCMV_1'}{\ECMV_2}}{\TUnknown}{\AMV}
   }
 
   \inferrule[ASEZipApL4]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\
+    \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\
     \matchedArrow{\TMV_1'}{\TMV_2}{\TMV_3} \\
     \ctxAnaType{\ctx}{\ECMV_2}{\TMV_2}
   }{
-    \ASEAction{\ctx}{\ZApL{\ECInconType{\ZMV_1}}{\ECMV_2}}{\TUnknown}{\ZApL{\ZMV_1'}{\ECMV_2}}{\TMV_3}{\AMV}
+    \ASEAction{\ctx}{\ZCApL{\ECInconType{\ZCMV_1}}{\ECMV_2}}{\TUnknown}{\ZCApL{\ZCMV_1'}{\ECMV_2}}{\TMV_3}{\AMV}
   }
 
   \inferrule[ASEZipApL5]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\
+    \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\
     \matchedArrow{\TMV_1'}{\TMV_2}{\TMV_3} \\
     \ctxNotAnaType{\ctx}{\ECMV_2}{\TMV_2}
   }{
-    \ASEAction{\ctx}{\ZApL{\ECInconType{\ZMV_1}}{\ECMV_2}}{\TUnknown}{\ZApL{\ZMV_1'}{\ECInconType{\ECMV_2}}}{\TMV_3}{\AMV}
+    \ASEAction{\ctx}{\ZCApL{\ECInconType{\ZCMV_1}}{\ECMV_2}}{\TUnknown}{\ZCApL{\ZCMV_1'}{\ECInconType{\ECMV_2}}}{\TMV_3}{\AMV}
   }
 
   \inferrule[ASEZipApL6]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\
+    \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\
     \notMatchedArrow{\TMV_1'}
   }{
-    \ASEAction{\ctx}{\ZApL{\ECInconType{\ZMV_1}}{\ECMV_2}}{\TUnknown}{\ZApL{\ECInconType{\ZMV_1'}}{\ECMV_2}}{\TUnknown}{\AMV}
+    \ASEAction{\ctx}{\ZCApL{\ECInconType{\ZCMV_1}}{\ECMV_2}}{\TUnknown}{\ZCApL{\ECInconType{\ZCMV_1'}}{\ECMV_2}}{\TUnknown}{\AMV}
   }
 
-  \inferrule[ASEZipApR]{
+  \inferrule[ASEZipApR1]{
     \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\
     \matchedArrow{\TMV_1}{\TMV_2}{\TMV_3} \\
-    \AAEAction{\ctx}{\ZMV_2}{\ZMV_2'}{\TMV_2}{\AMV}
+    \AAEAction{\ctx}{\ZCMV_2}{\ZCMV_2'}{\TMV_2}{\AMV}
   }{
-    \ASEAction{\ctx}{\ZApR{\ECMV_1}{\ZMV_2}}{\TMV}{\ZApR{\ECMV_1}{\ZMV_2'}}{\TMV_3}{\AMV}
+    \ASEAction{\ctx}{\ZCApR{\ECMV_1}{\ZCMV_2}}{\TMV}{\ZCApR{\ECMV_1}{\ZCMV_2'}}{\TMV_3}{\AMV}
+  }
+
+  \inferrule[ASEZipApR2]{
+    \AAEAction{\ctx}{\ZCMV_2}{\ZCMV_2'}{\TUnknown}{\AMV}
+  }{
+    \ASEAction{\ctx}{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCMV_2}}{\TUnknown}{\ZCApSynNonMatchedArrowR{\ECMV_1}{\ZCMV_2'}}{\TUnknown}{\AMV}
   }
 
   \inferrule[ASEZipLetL1]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\
-    \consistent{\TMV_1}{\TMV_1'}
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\
+    \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\
+    \equal{\TMV_1}{\TMV_1'}
   }{
-    \ASEAction{\ctx}{\ZLetL{x}{\ZMV_1}{\ECMV_2}}{\TMV_2}{\ZLetL{x}{\ZMV_1'}{\ECMV_2}}{\TMV_2}{\AMV}
+    \ASEAction{\ctx}{\ZCLetL{x}{\ZCMV_1}{\ECMV_2}}{\TMV_2}{\ZCLetL{x}{\ZCMV_1'}{\ECMV_2}}{\TMV_2}{\AMV}
   }
 
   \inferrule[ASEZipLetL2]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV_1}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV_1}{\TMV_1}{\ZMV_1'}{\TMV_1'}{\AMV} \\\\
-    \inconsistent{\TMV_1}{\TMV_1'} \\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\
+    \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\
+    \notEqual{\TMV_1}{\TMV_1'} \\
     \ctxSynFixedInto{\extendCtx{\ctx}{x}{\TMV_1'}}{\erase{\ECMV_2}}{\ECMV_2'}{\TMV_2'}
   }{
-    \ASEAction{\ctx}{\ZLetL{x}{\ZMV_1}{\ECMV_2}}{\TMV_2}{\ZLetL{x}{\ZMV_1'}{\ECMV_2'}}{\TMV_2'}{\AMV}
+    \ASEAction{\ctx}{\ZCLetL{x}{\ZCMV_1}{\ECMV_2}}{\TMV_2}{\ZCLetL{x}{\ZCMV_1'}{\ECMV_2'}}{\TMV_2'}{\AMV}
   }
 
   \inferrule[ASEZipLetR]{
     \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\
-    \ctxSynTypeM{\extendCtx{\ctx}{x}{\TMV_1}}{\cursorErase{\ZMV_2}}{\TMV_2} \\\\
-    \ASEAction{\extendCtx{\ctx}{x}{\TMV_1}}{\ZMV_2}{\TMV_2}{\ZMV_2'}{\TMV_2'}{\AMV}
+    \ctxSynTypeM{\extendCtx{\ctx}{x}{\TMV_1}}{\cursorErase{\ZCMV_2}}{\TMV_2} \\\\
+    \ASEAction{\extendCtx{\ctx}{x}{\TMV_1}}{\ZCMV_2}{\TMV_2}{\ZCMV_2'}{\TMV_2'}{\AMV}
   }{
-    \ASEAction{\ctx}{\ZLetR{x}{\ECMV_1}{\ZMV_2}}{\TMV_2}{\ZLetR{x}{\ECMV_1}{\ZMV_2'}}{\TMV_2'}{\AMV}
+    \ASEAction{\ctx}{\ZCLetR{x}{\ECMV_1}{\ZCMV_2}}{\TMV_2}{\ZCLetR{x}{\ECMV_1}{\ZCMV_2'}}{\TMV_2'}{\AMV}
   }
 
   \inferrule[ASEZipPlusL]{
-    \AAEAction{\ctx}{\ZMV}{\ZMV'}{\TNum}{\AMV}
+    \AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TNum}{\AMV}
   }{
-    \ASEAction{\ctx}{\ZPlusL{\ZMV}{\ECMV}}{\TNum}{\ZPlusL{\ZMV'}{\ECMV}}{\TNum}{\AMV}
+    \ASEAction{\ctx}{\ZCPlusL{\ZCMV}{\ECMV}}{\TNum}{\ZCPlusL{\ZCMV'}{\ECMV}}{\TNum}{\AMV}
   }
 
   \inferrule[ASEZipPlusR]{
-    \AAEAction{\ctx}{\ZMV}{\ZMV'}{\TNum}{\AMV}
+    \AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TNum}{\AMV}
   }{
-    \ASEAction{\ctx}{\ZPlusR{\ECMV}{\ZMV}}{\TNum}{\ZPlusR{\ECMV}{\ZMV'}}{\TNum}{\AMV}
+    \ASEAction{\ctx}{\ZCPlusR{\ECMV}{\ZCMV}}{\TNum}{\ZCPlusR{\ECMV}{\ZCMV'}}{\TNum}{\AMV}
   }
 
   \inferrule[ASEZipIfC]{
-    \AAEAction{\ctx}{\ZMV}{\ZMV'}{\TBool}{\AMV}
+    \AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TBool}{\AMV}
   }{
-    \ASEAction{\ctx}{\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2}}{\TMV}{\ZIfC{\ZMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV}
+    \ASEAction{\ctx}{\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\TMV}{\ZCIfC{\ZCMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV}
   }
 
   \inferrule[ASEZipIfL1]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_1} \\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\\\
-    \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\
-    \consistent{\TMV_1'}{\TMV_2}
+    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\
+    \consistent{\TMV_1'}{\TMV_2} \\
+    \TMV' = \TMeet{\TMV_1'}{\TMV_2}
   }{
-    \ASEAction{\ctx}{\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2}}{\TMV}{\ZIfL{\ECMV_1}{\ZMV'}{\ECMV_2}}{\TMeet{\TMV_1'}{\TMV_2}}{\AMV}
+    \ASEAction{\ctx}{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMV'}{\AMV}
   }
 
   \inferrule[ASEZipIfL2]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_1} \\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\\\
-    \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\
+    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\
     \inconsistent{\TMV_1'}{\TMV_2}
   }{
-    \ASEAction{\ctx}{\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2}}{\TMV}{\ZInconBrL{\ECMV_1}{\ZMV'}{\ECMV_2}}{\TUnknown}{\AMV}
+    \ASEAction{\ctx}{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCInconBrL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TUnknown}{\AMV}
   }
 
   \inferrule[ASEZipIfR1]{
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_1} \\
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_2} \\\\
-    \ASEAction{\ctx}{\ZMV}{\TMV_2}{\ZMV'}{\TMV_2'}{\AMV} \\
-    \consistent{\TMV_1}{\TMV_2'}
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_2} \\\\
+    \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\
+    \consistent{\TMV_1}{\TMV_2'} \\
+    \TMV' = \TMeet{\TMV_1}{\TMV_2'}
   }{
-    \ASEAction{\ctx}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV}}{\TMV}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV'}}{\TMeet{\TMV_1}{\TMV_2'}}{\AMV}
+    \ASEAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMV'}{\AMV}
   }
 
   \inferrule[ASEZipIfR2]{
     \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_2} \\\\
-    \ASEAction{\ctx}{\ZMV}{\TMV_2}{\ZMV'}{\TMV_2'}{\AMV} \\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_2} \\\\
+    \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\
     \inconsistent{\TMV_1}{\TMV_2'}
   }{
-    \ASEAction{\ctx}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV}}{\TMV}{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV'}}{\TUnknown}{\AMV}
+    \ASEAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TUnknown}{\AMV}
   }
 
   \inferrule[ASEZipInconsistentBranchesC]{
-    \AAEAction{\ctx}{\ZMV}{\ZMV'}{\TBool}{\AMV}
+    \AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TBool}{\AMV}
   }{
-    \ASEAction{\ctx}{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}}{\TMV}{\ZInconBrC{\ZMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV}
+    \ASEAction{\ctx}{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\TMV}{\ZCInconBrC{\ZCMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV}
   }
 
   \inferrule[ASEZipInconsistentBranchesL1]{
-    \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\
+    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\
-    \consistent{\TMV_1'}{\TMV_2}
+    \consistent{\TMV_1'}{\TMV_2} \\
+    \TMV' = \TMeet{\TMV_1'}{\TMV_2}
   }{
-    \ASEAction{\ctx}{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}{\TMV}{\ZIfL{\ECMV_1}{\ZMV'}{\ECMV_2}}{\TMeet{\TMV_1'}{\TMV_2}}{\AMV}
+    \ASEAction{\ctx}{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMV'}{\AMV}
   }
 
   \inferrule[ASEZipInconsistentBranchesL2]{
-    \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\
+    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\
     \inconsistent{\TMV_1'}{\TMV_2}
   }{
-    \ASEAction{\ctx}{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}{\TMV}{\ZInconBrL{\ECMV_1}{\ZMV'}{\ECMV_2}}{\TUnknown}{\AMV}
+    \ASEAction{\ctx}{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCInconBrL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TUnknown}{\AMV}
   }
 
   \inferrule[ASEZipInconsistentBranchesR1]{
-    \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV}{\TMV_2}{\ZMV'}{\TMV_2'}{\AMV} \\
-    \consistent{\TMV_1}{\TMV_2'}
+    \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\\\
+    \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\
+    \consistent{\TMV_1}{\TMV_2'} \\
+    \TMV' = \TMeet{\TMV_1}{\TMV_2'}
   }{
-    \ASEAction{\ctx}{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}{\TMV}{\ZIfL{\ECMV_1}{\ECMV_2}{\ZMV'}}{\TMeet{\TMV_1}{\TMV_2'}}{\AMV}
+    \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMV'}{\AMV}
   }
 
   \inferrule[ASEZipInconsistentBranchesR2]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\\\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV}{\TMV_2}{\ZMV'}{\TMV_2'}{\AMV} \\
     \inconsistent{\TMV_1}{\TMV_2'}
   }{
-    \ASEAction{\ctx}{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}{\TMV}{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV'}}{\TUnknown}{\AMV}
+    \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TUnknown}{\AMV}
+  }
+
+  \inferrule[ASEZipPairL]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV}
+  }{
+    \ASEAction{\ctx}{\ZCPairL{\ZCMV}{\ECMV}}{\TProd{\TMV_1}{\TMV_2}}{\ZCPairL{\ZCMV'}{\ECMV}}{\TProd{\TMV_1'}{\TMV_2}}{\AMV}
+  }
+
+  \inferrule[ASEZipPairR]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV}
+  }{
+    \ASEAction{\ctx}{\ZCPairR{\ECMV}{\ZCMV}}{\TProd{\TMV_1}{\TMV_2}}{\ZCPairR{\ECMV}{\ZCMV'}}{\TProd{\TMV_1'}{\TMV_2}}{\AMV}
+  }
+
+  \inferrule[ASEZipProjL1]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\
+    \matchedProd{\TMV'}{\TMV_1'}{\TMV_2'}
+  }{
+    \ASEAction{\ctx}{\ZCProjL{\ZCMV}}{\TMV_1}{\ZCProjL{\ZCMV'}}{\TMV_1'}{\AMV}
+  }
+
+  \inferrule[ASEZipProjL2]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\
+    \notMatchedProd{\TMV'}
+  }{
+    \ASEAction{\ctx}{\ZCProjL{\ZCMV}}{\TMV_1}{\ZCProjLSynNonMatchedProd{\ZCMV'}}{\TUnknown}{\AMV}
+  }
+
+  \inferrule[ASEZipProjL3]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\
+    \matchedProd{\TMV'}{\TMV_1'}{\TMV_2'}
+  }{
+    \ASEAction{\ctx}{\ZCProjLSynNonMatchedProd{\ZCMV}}{\TUnknown}{\ZCProjL{\ZCMV'}}{\TMV_1'}{\AMV}
+  }
+
+  \inferrule[ASEZipProjL4]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\
+    \notMatchedProd{\TMV'}
+  }{
+    \ASEAction{\ctx}{\ZCProjLSynNonMatchedProd{\ZCMV}}{\TUnknown}{\ZCProjLSynNonMatchedProd{\ZCMV'}}{\TUnknown}{\AMV}
+  }
+
+  \inferrule[ASEZipProjR1]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\
+    \matchedProd{\TMV'}{\TMV_1'}{\TMV_2'}
+  }{
+    \ASEAction{\ctx}{\ZCProjR{\ZCMV}}{\TMV_2}{\ZCProjR{\ZCMV'}}{\TMV_2'}{\AMV}
+  }
+
+  \inferrule[ASEZipProjR2]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\
+    \notMatchedProd{\TMV'}
+  }{
+    \ASEAction{\ctx}{\ZCProjR{\ZCMV}}{\TMV_2}{\ZCProjRSynNonMatchedProd{\ZCMV'}}{\TUnknown}{\AMV}
+  }
+
+  \inferrule[ASEZipProjL3]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\
+    \matchedProd{\TMV'}{\TMV_1'}{\TMV_2'}
+  }{
+    \ASEAction{\ctx}{\ZCProjRSynNonMatchedProd{\ZCMV}}{\TUnknown}{\ZCProjR{\ZCMV'}}{\TMV_2'}{\AMV}
+  }
+
+  \inferrule[ASEZipProjR4]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\
+    \notMatchedProd{\TMV'}
+  }{
+    \ASEAction{\ctx}{\ZCProjRSynNonMatchedProd{\ZCMV}}{\TUnknown}{\ZCProjRSynNonMatchedProd{\ZCMV'}}{\TUnknown}{\AMV}
   }
 \end{mathparpagebreakable}
 
 \subsubsection{Analytic expression actions}
 \label{sec:typed-analytic-expression-actions}
-\judgbox{\ensuremath{\AAAction{\ctx}{\ZMV}{\ZMV'}{\TMV'}{\AMV}}}
+\judgbox{\ensuremath{\AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV'}{\AMV}}}
 
 \paragraph{Subsumption}
 \begin{mathpar}
   \inferrule[AAESubsume1]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV'} \\
-    \ASAction{\ctx}{\ZMV}{\TMV'}{\ZMV'}{\TMV''}{\AMV} \\\\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\
+    \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\
     \consistent{\TMV}{\TMV''} \\
-    \subsumable{\cursorErase{\ZMV}}
+    \subsumable{\cursorErase{\ZCMV}}
   }{
-    \AAAction{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}
   }
 
   \inferrule[AAESubsume2]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV'} \\
-    \ASAction{\ctx}{\ZMV}{\TMV'}{\ZMV'}{\TMV''}{\AMV} \\\\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\
+    \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\
     \inconsistent{\TMV}{\TMV''} \\
-    \subsumable{\cursorErase{\ZMV}}
+    \subsumable{\cursorErase{\ZCMV}}
   }{
-    \AAAction{\ctx}{\ZMV}{\ZInconType{\ZMV'}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCMV}{\ZCInconType{\ZCMV'}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEInconsistentTypes1]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV'} \\
-    \ASAction{\ctx}{\ZMV}{\TMV'}{\ZMV'}{\TMV''}{\AMV} \\\\
-    \inconsistent{\TMV}{\TMV''} \\
-    \subsumable{\cursorErase{\ZMV}}
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\
+    \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\
+    \consistent{\TMV}{\TMV''} \\
+    \subsumable{\cursorErase{\ZCMV}}
   }{
-    \AAAction{\ctx}{\ZInconType{\ZMV}}{\ZInconType{\ZMV'}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCMV'}{\TMV}{\AMV}
   }
 
   \inferrule[AAEInconsistentTypes2]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV'} \\
-    \ASAction{\ctx}{\ZMV}{\TMV'}{\ZMV'}{\TMV''}{\AMV} \\\\
-    \consistent{\TMV}{\TMV''} \\
-    \subsumable{\cursorErase{\ZMV}}
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV'} \\
+    \ASAction{\ctx}{\ZCMV}{\TMV'}{\ZCMV'}{\TMV''}{\AMV} \\\\
+    \inconsistent{\TMV}{\TMV''} \\
+    \subsumable{\cursorErase{\ZCMV}}
   }{
-    \AAAction{\ctx}{\ZInconType{\ZMV}}{\ZMV'}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCInconType{\ZCMV}}{\ZCInconType{\ZCMV'}}{\TMV}{\AMV}
   }
 \end{mathpar}
 
 \paragraph{Movement}
 \begin{mathpar}
   \inferrule[AAEMove]{
-    \ASEMove{\ZMV}{\ZMV'}{\MMV}
+    \ASEMove{\ZCMV}{\ZCMV'}{\MMV}
   }{
-    \AAMove{\ctx}{\ZMV}{\ZMV'}{\TMV}{\MMV}
+    \AAMove{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\MMV}
   }
 \end{mathpar}
 
@@ -767,113 +1062,230 @@ \subsubsection{Analytic expression actions}
 \begin{mathparpagebreakable}
   \inferrule[AAEConLam1]{
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\
-    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\ECMV}{\ECMV'}{\TMV_2}
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
   }{
-    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZLamT{x}{\ZTCursor{\TMV_1}}{\ECMV'}}{\TMV}{\SLam{x}}
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLamT{x}{\ZTCursor{\TMV_1}}{\ECMV'}}{\TMV}{\SLam{x}}
   }
 
   \inferrule[AAEConLam2]{
     \notMatchedArrow{\TMV} \\
-    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\ECMV}{\ECMV'}{\TUnknown}
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
   }{
-    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZInconType{\ZLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}}{\TMV}{\SLam{x}}
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}{\TMV}{\SLam{x}}
   }
 
-  \inferrule[AAEConLetL]{ }{
-    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZLetL{x}{\ECMV}{\ZCursor{\ECEHole}}}{\TMV}{\SLetL{x}}
+  \inferrule[AAEConLetL]{
+    \ctxSynFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TMV}
+  }{
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLetL{x}{\ECMV'}{\ZCCursor{\ECEHole}}}{\TMV}{\SLetL{x}}
   }
 
   \inferrule[AAEConLetR]{
     \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TMV}
   }{
-    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZLetR{x}{\ZCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SLetR{x}}
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLetR{x}{\ZCCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SLetR{x}}
+  }
+ 
+  \inferrule[AAEConIfC]{
+    \ctxAnaFixedInto{\ctx}{\ECMV}{\ECMV'}{\TBool}
+  }{
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfL{\ECMV'}{\ZCCursor{\ECEHole}}{\ECEHole}}{\TMV}{\SIfC}
   }
  
   \inferrule[AAEConIfL]{ }{
-    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZIfC{\ZCursor{\ECEHole}}{\ECMV}{\ECEHole}}{\TMV}{\SIfL}
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECMV'}{\ECEHole}}{\TMV}{\SIfL}
+  }
+
+  \inferrule[AAEConIfR]{ }{
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCIfC{\ZCCursor{\ECEHole}}{\ECEHole}{\ECMV'}}{\TMV}{\SIfR}
   }
 
-  \inferrule[AAEConIfR]{
+  \inferrule[AAEConPairL1]{
+    \matchedProd{\TMV}{\TMV_1}{\TMV_2} \\
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TMV_1}
   }{
-    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZIfC{\ZCursor{\ECEHole}}{\ECEHole}{\ECMV}}{\TMV}{\SIfR}
+    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairL{\ECMV'}{\ZCursor{\ECEHole}}}{\TMV}{\SPairL}
+  }
+
+  \inferrule[AAEConPairL2]{
+    \notMatchedProd{\TMV} \\
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
+  }{
+    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairAnaNonMatchedProdL{\ECMV'}{\ZCursor{\ECEHole}}}{\TMV}{\SPairL}
+  }
+
+  \inferrule[AAEConPairR1]{
+    \matchedProd{\TMV}{\TMV_1}{\TMV_2} \\
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+  }{
+    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairR{\ZCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SPairR}
+  }
+
+  \inferrule[AAEConPairR2]{
+    \notMatchedProd{\TMV} \\
+    \ctxAnaFixedInto{\ctx}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
+  }{
+    \AACon{\ctx}{\ZCursor{\ECMV}}{\ZCPairAnaNonMatchedProdR{\ZCursor{\ECEHole}}{\ECMV'}}{\TMV}{\SPairR}
   }
 \end{mathparpagebreakable}
 
 \paragraph{Zipper Cases} \ \\
 \begin{mathparpagebreakable}
   \inferrule[AAEZipLamT1]{
-    \AUTAction{\ZTMV}{\ZTMV'}{\AMV} \\
-    \consistent{\cursorErase{\ZTMV}}{\cursorErase{\ZTMV'}}
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}}
   }{
-    \AAAction{\ctx}{\ZLamT{x}{\ZTMV}{\ECMV}}{\ZLamT{x}{\ZTMV'}{\ECMV}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLamT2]{
-    \AUTAction{\ZTMV}{\ZTMV'}{\AMV} \\
-    \inconsistent{\cursorErase{\ZTMV}}{\cursorErase{\ZTMV'}} \\
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
-    \consistent{\cursorErase{\ZTMV'}}{\TMV_1} \\
-    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+    \consistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
   }{
-    \AAAction{\ctx}{\ZLamT{x}{\ZTMV}{\ECMV}}{\ZLamT{x}{\ZTMV'}{\ECMV'}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLamT3]{
-    \AUTAction{\ZTMV}{\ZTMV'}{\AMV} \\
-    \inconsistent{\cursorErase{\ZTMV}}{\cursorErase{\ZTMV'}} \\
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV'}} \\
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
-    \inconsistent{\cursorErase{\ZTMV'}}{\TMV_1} \\
-    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+    \inconsistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+  }{
+    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT4]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}}
   }{
-    \AAAction{\ctx}{\ZLamT{x}{\ZTMV}{\ECMV}}{\ZInconType{\ZLamT{x}{\ZTMV'}{\ECMV'}}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
   }
 
-  \inferrule[AAEZipLamE]{
+  \inferrule[AAEZipLamT5]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\\\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
+  }{
+    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT6]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}}
+  }{
+    \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT7]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\
+    \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
+    \consistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+  }{
+    \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT8]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\
+    \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
+    \inconsistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+  }{
+    \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamE1]{
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\
-    \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZMV}{\ZMV'}{\TMV_2}{\AMV}
+    \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TMV_2}{\AMV}
+  }{
+    \AAAction{\ctx}{\ZCLamE{x}{\TMV_3}{\ZCMV}}{\ZCLamE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamE2]{
+    \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TUnknown}{\AMV}
   }{
-    \AAAction{\ctx}{\ZLamE{x}{\TMV_3}{\ZMV}}{\ZLamE{x}{\TMV_3}{\ZMV'}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowE{x}{\TMV_3}{\ZCMV}}{\ZCLamAnaNonMatchedArrowE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamE3]{
+    \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\
+    \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TMV_2}{\AMV}
+  }{
+    \AAAction{\ctx}{\ZCLamInconAscE{x}{\TMV_3}{\ZCMV}}{\ZCLamInconAscE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLetL1]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\
-    \consistent{\TMV_1}{\TMV_1'}
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\
+    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\
+    \equal{\TMV_1}{\TMV_1'}
   }{
-    \AAAction{\ctx}{\ZLetL{x}{\ZMV}{\ECMV}}{\ZLetL{x}{\ZMV'}{\ECMV}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLetL{x}{\ZCMV}{\ECMV}}{\ZCLetL{x}{\ZCMV'}{\ECMV}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLetL2]{
-    \ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZMV}{\TMV_1}{\ZMV'}{\TMV_1'}{\AMV} \\\\
+    \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\
+    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\
+    \notEqual{\TMV_1}{\TMV_1'} \\
     \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1'}}{\erase{\ECMV}}{\ECMV'}{\TMV}
   }{
-    \AAAction{\ctx}{\ZLetL{x}{\ZMV}{\ECMV}}{\ZLetL{x}{\ZMV'}{\ECMV'}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLetL{x}{\ZCMV}{\ECMV}}{\ZCLetL{x}{\ZCMV'}{\ECMV'}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLetR]{
-    \ctxSynTypeM{\ctx}{\ECMV}{\TMV'} \\
-    \AAAction{\extendCtx{\ctx}{x}{\TMV'}}{\ZMV}{\ZMV'}{\TMV}{\AMV}
+    \ctxSynTypeM{\ctx}{\ECMV}{\TMV_1} \\
+    \AAAction{\extendCtx{\ctx}{x}{\TMV_1}}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}
   }{
-    \AAAction{\ctx}{\ZLetR{x}{\ECMV}{\ZMV}}{\ZLetL{x}{\ECMV}{\ZMV'}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLetR{x}{\ECMV}{\ZCMV}}{\ZCLetL{x}{\ECMV}{\ZCMV'}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipIfC]{
-    \AAAction{\ctx}{\ZMV}{\ZMV'}{\TBool}{\AMV}
+    \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TBool}{\AMV}
   }{
-    \AAAction{\ctx}{\ZIfC{\ZMV}{\ECMV_1}{\ECMV_2}}{\ZIfC{\ZMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\ZCIfC{\ZCMV'}{\ECMV_1}{\ECMV_2}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipIfL]{
-    \AAAction{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}
   }{
-    \AAAction{\ctx}{\ZIfL{\ECMV_1}{\ZMV}{\ECMV_2}}{\ZIfL{\ECMV_1}{\ZMV'}{\ECMV_2}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipIfR]{
-    \AAAction{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}
+  }{
+    \AAAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipPairL1]{
+    \matchedProd{\TMV}{\TMV_1}{\TMV_2} \\
+    \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV_1}{\AMV}
+  }{
+    \AAAction{\ctx}{\ZCPairL{\ZCMV}{\ECMV}}{\ZCPairL{\ZCMV'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipPairL2]{
+    \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TUnknown}{\AMV}
+  }{
+    \AAAction{\ctx}{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}}{\ZCPairAnaNonMatchedProdL{\ZCMV'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipPairR1]{
+    \matchedProd{\TMV}{\TMV_1}{\TMV_2} \\
+    \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV_2}{\AMV}
+  }{
+    \AAAction{\ctx}{\ZCPairR{\ECMV}{\ZCMV}}{\ZCPairR{\ECMV}{\ZCMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipPairR2]{
+    \AAAction{\ctx}{\ZCMV}{\ZCMV'}{\TUnknown}{\AMV}
   }{
-    \AAAction{\ctx}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV}}{\ZIfR{\ECMV_1}{\ECMV_2}{\ZMV'}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}}{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV'}}{\TMV}{\AMV}
   }
 \end{mathparpagebreakable}
 
@@ -881,109 +1293,209 @@ \subsubsection{Iterated actions}
 \label{sec:typed-iterated-actions}
 The iterated type action and movements judgments are the same as in the untyped model. \\
 
-\judgbox{\ensuremath{\ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AIMV}}}
+\judgbox{\ensuremath{\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AIMV}}}
 %
 \begin{mathpar}
   \inferrule[ASEIRefl]{ }{
-    \ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV}{\TMV}{\AINil}
+    \ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV}{\TMV}{\AINil}
   }
 
   \inferrule[ASEIExp]{
-    \ASEAction{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AMV} \\
-    \ASEActionIter{\ctx}{\ZMV'}{\TMV'}{\ZMV''}{\TMV''}{\AIMV}
+    \ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV} \\
+    \ASEActionIter{\ctx}{\ZCMV'}{\TMV'}{\ZCMV''}{\TMV''}{\AIMV}
   }{
-    \ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV''}{\TMV''}{\AICons{\AMV}{\AIMV}}
+    \ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV''}{\TMV''}{\AICons{\AMV}{\AIMV}}
   }
 \end{mathpar}
 
-\judgbox{\ensuremath{\AAEActionIter{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AIMV}}}
+\judgbox{\ensuremath{\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AIMV}}}
 %
 \begin{mathpar}
   \inferrule[AAEIRefl]{ }{
-    \AAEActionIter{\ctx}{\ZMV}{\ZMV}{\TMV}{\AINil}
+    \AAEActionIter{\ctx}{\ZCMV}{\ZCMV}{\TMV}{\AINil}
   }
 
   \inferrule[AAEIExp]{
-    \AAEAction{\ctx}{\ZMV}{\ZMV'}{\TMV'}{\AMV} \\
-    \AAEActionIter{\ctx}{\ZMV'}{\ZMV''}{\TMV''}{\AIMV}
+    \AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV'}{\AMV} \\
+    \AAEActionIter{\ctx}{\ZCMV'}{\ZCMV''}{\TMV''}{\AIMV}
   }{
-    \AAEActionIter{\ctx}{\ZMV}{\ZMV''}{\TMV''}{\AICons{\AMV}{\AIMV}}
+    \AAEActionIter{\ctx}{\ZCMV}{\ZCMV''}{\TMV''}{\AICons{\AMV}{\AIMV}}
   }
 \end{mathpar}
 
+\subsection{Mark erasure}
+\label{sec:typed-mark-erasure}
+\judgbox{\ensuremath{\erase{\ZCMV}}} is a metafunction $\ZCMName \to \ZMName$ defined as follows:
+%
+\newcommand{\erasesToRow}[2]{\erase{#1} & = & #2}
+\[\begin{array}{rcl}
+  \erasesToRow{\ZCCursor{\ECMV}}{\ZCCursor{\erase{\ECMV}}} \\
+  \erasesToRow{(\ZCLamT{x}{\ZTMV}{\ECMV})}{\ZCLamT{x}{\ZTMV}{(\erase{\ECMV})}} \\
+  \erasesToRow{(\ZCLamE{x}{\TMV}{\ZCMV})}{\ZCLamE{x}{\TMV}{(\erase{\ZCMV})}} \\
+  \erasesToRow{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}{\ZCLamT{x}{\ZTMV}{(\erase{\ECMV})}} \\
+  \erasesToRow{\ZCLamAnaNonMatchedArrowE{x}{\TMV}{\ZCMV}}{\ZCLamE{x}{\TMV}{(\erase{\ZCMV})}} \\
+  \erasesToRow{\ZCLamInconAscT{x}{\ZTMV}{\ECMV}}{\ZCLamT{x}{\ZTMV}{(\erase{\ECMV})}} \\
+  \erasesToRow{\ZCLamInconAscE{x}{\TMV}{\ZCMV}}{\ZCLamE{x}{\TMV}{(\erase{\ZCMV})}} \\
+  \erasesToRow{(\ZCApL{\ZCMV}{\ECMV})}{\ZCApL{(\erase{\ZCMV})}{(\erase{\ZCMV})}} \\
+  \erasesToRow{(\ZCApR{\ECMV}{\ZCMV})}{\ZCApR{(\erase{\ECMV})}{(\erase{\ZCMV})}} \\
+  \erasesToRow{(\ZCApSynNonMatchedArrowL{\ZCMV}{\ECMV})}{\ZCApL{\erase{\ZCMV}}{(\erase{\ECMV})}} \\
+  \erasesToRow{(\ZCApSynNonMatchedArrowR{\ECMV}{\ZCMV})}{\ZCApR{\erase{\ECMV}}{(\erase{\ZCMV})}} \\
+  \erasesToRow{(\ZCLetL{x}{\ZCMV}{\ECMV})}{\ZCLetL{x}{(\erase{\ZCMV})}{(\erase{\ECMV})}} \\
+  \erasesToRow{(\ZCLetR{x}{\ECMV}{\ZCMV})}{\ZCLetR{x}{(\erase{\ECMV})}{(\erase{\ZCMV})}} \\
+  \erasesToRow{(\ZCPlusL{\ZCMV}{\ECMV})}{\ZCPlusL{(\erase{\ZCMV})}{(\erase{\ECMV})}} \\
+  \erasesToRow{(\ZCPlusR{\ECMV}{\ZCMV})}{\ZCPlusR{(\erase{\ECMV})}{(\erase{\ZCMV})}} \\
+  \erasesToRow{(\ZCIfC{\ZCMV}{\ECMV_1}{\ECMV_2})}{\ZCIfC{(\erase{\ZCMV})}{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}} \\
+  \erasesToRow{(\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2})}{\ZCIfL{(\erase{\ECMV_1})}{(\erase{\ZCMV})}{(\erase{\ECMV_2})}} \\
+  \erasesToRow{(\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV})}{\ZCIfR{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}{(\erase{\ZCMV})}} \\
+  \erasesToRow{\ZCInconBrC{\ZCMV}{\ECMV_1}{\ECMV_2}}{\ZCIfC{(\erase{\ZCMV})}{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}} \\
+  \erasesToRow{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\ZCIfL{(\erase{\ECMV_1})}{(\erase{\ZCMV})}{(\erase{\ECMV_2})}} \\
+  \erasesToRow{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\ZCIfR{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}{(\erase{\ZCMV})}} \\
+  \erasesToRow{\ZCPairL{\ZCMV}{\ECMV}}{\ZCPairL{\erase{\ZCMV}}{\erase{\ECMV}}} \\
+  \erasesToRow{\ZCPairR{\ECMV}{\ZCMV}}{\ZCPairR{\erase{\ECMV}}{\erase{\ZCMV}}} \\
+  \erasesToRow{\ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV}}{\ZCPairL{\erase{\ZCMV}}{\erase{\ECMV}}} \\
+  \erasesToRow{\ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}}{\ZCPairR{\erase{\ECMV}}{\erase{\ZCMV}}} \\
+  \erasesToRow{(\ZCProjL{\ZCMV})}{\ZCProjL{(\erase{\ZCMV})}} \\
+  \erasesToRow{(\ZCProjLSynNonMatchedProd{\ZCMV})}{\ZCProjL{\erase{\ZCMV}}} \\
+  \erasesToRow{(\ZCProjR{\ZCMV})}{\ZCProjR{(\erase{\ZCMV})}} \\
+  \erasesToRow{(\ZCProjRSynNonMatchedProd{\ZCMV})}{\ZCProjR{\erase{\ZCMV}}} \\
+  \erasesToRow{\ZCInconType{\ZCMV}}{\erase{\ZCMV}} \\
+\end{array}\]
+
 \subsection{Metatheorems}
 \label{sec:typed-metatheorems}
-\begin{theorem}[name=Sensibility] \
+\begin{theorem}[name=Erasure Commutativity]
+  For all $\ZCMV$, $\cursorErase{(\erase{\ZCMV})} = \erase{(\cursorErase{\ZCMV})}$.
+  %
+  \[\begin{tikzcd}
+    \ZCMV \mathsmaller{~\in~ \ZCMName} && \ZMV \mathsmaller{~\in~ \ZMName} \\\\
+    \ECMV \mathsmaller{~\in~ \ECMName} && \EMV \mathsmaller{~\in~ \EMName}
+    \arrow["{\cursorErase{\_}}"', from=1-1, to=3-1]
+    \arrow["{\erase{\_}}", from=1-1, to=1-3]
+    \arrow["{\cursorErase{\_}}", from=1-3, to=3-3]
+    \arrow["{\erase{\_}}"', from=3-1, to=3-3]
+  \end{tikzcd}\]
+\end{theorem}
+
+\begin{theorem}[name=Correctness] \
   \begin{enumerate}
-    \item If $\zWellFormed{\ZMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and
-      $\ASEAction{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AMV}$, then $\zWellFormed{\ZMV'}$ and
-      $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV'}}{\TMV'}$.
+    \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}
 
-    \item If $\zWellFormed{\ZMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and
-      $\AAEAction{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMV}$, then $\zWellFormed{\ZMV'}$ and
-      $\ctxAnaType{\ctx}{\cursorErase{\ZMV'}}{\TMV}$.
+\begin{theorem}[name=Sensibility] \
+  \begin{enumerate}
+    \item If $\zWellFormed{\ZCMV}$
+        and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$,
+      then $\zWellFormed{\ZCMV'}$
+        and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV'}}{\TMV'}$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$,
+      then $\zWellFormed{\ZCMV'}$
+        and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV'}}{\TMV}$.
   \end{enumerate}
 \end{theorem}
 
 \begin{theorem}[name=Movement Erasure Invariance] \
   \begin{enumerate}
-    \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZTMV} =
-      \cursorErase{\ZTMV'}$.
-
-    \item If $\zWellFormed{\ZMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and
-      $\ASEAction{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AMove{\MMV}}$, then $\zWellFormed{\ZMV'}$ and
-      $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$ and $\equal{\TMV}{\TMV'}$.
-
-    \item If $\zWellFormed{\ZMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and
-      $\AAEAction{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMove{\MMV}}$, then $\zWellFormed{\ZMV'}$ and
-      $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$.
+    \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$,
+      then $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMove{\MMV}}$,
+      then $\zWellFormed{\ZCMV'}$
+        and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$
+        and $\equal{\TMV}{\TMV'}$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMove{\MMV}}$,
+      then $\zWellFormed{\ZCMV'}$
+        and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$.
   \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 $\zWellFormed{\ZMV}$ and $\zWellFormed{\ZMV'}$ and
-      $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$,
-      then there exists $\AIMV$ such that $\movements{\AIMV}$ and
-      $\ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV}{\AIMV}$.
-
-    \item If $\zWellFormed{\ZMV}$ and $\zWellFormed{\ZMV'}$ and
-      $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$,
-      then there exists $\AIMV$ such that $\movements{\AIMV}$ and
-      $\AAEActionIter{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AIMV}$.
+    \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\zWellFormed{\ZCMV'}$
+        and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV}{\AIMV}$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\zWellFormed{\ZCMV'}$
+        and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\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 $\zWellFormed{\ZMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and
-      $\cursorErase{\ZMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and
-      $\ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZTCursor{\ECMV}}{\TMV}{\AIMV}$.
-
-    \item If $\zWellFormed{\ZMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and
-      $\cursorErase{\ZMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and
-      $\AAEActionIter{\ctx}{\ZMV}{\ZTCursor{\ECMV}}{\TMV}{\AIMV}$.
+    \item If $\cursorErase{\ZTMV} = \TMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\cursorErase{\ZCMV} = \ECMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\cursorErase{\ZCMV} = \ECMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AAEActionIter{\ctx}{\ZCMV}{\ZCCursor{\ECMV}}{\TMV}{\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 $\zWellFormed{\ZMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and
-      $\cursorErase{\ZMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and
-      $\ASEActionIter{\ctx}{\ZTCursor{\ECMV}}{\TMV}{\ZMV}{\TMV}{\AIMV}$.
-
-    \item If $\zWellFormed{\ZMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and
-      $\cursorErase{\ZMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and
-      $\AAEActionIter{\ctx}{\ZTCursor{\ECMV}}{\ZMV}{\TMV}{\AIMV}$.
+    \item If $\cursorErase{\ZTMV} = \TMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\cursorErase{\ZCMV} = \ECMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\ASEActionIter{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCMV}{\TMV}{\AIMV}$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\cursorErase{\ZCMV} = \ECMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AAEActionIter{\ctx}{\ZCCursor{\ECMV}}{\ZCMV}{\TMV}{\AIMV}$.
   \end{enumerate}
 \end{lemma}
 
@@ -993,26 +1505,31 @@ \subsection{Metatheorems}
       $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$.
 
     \item If $\ctxSynTypeM{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that
-      $\ASEActionIter{\ctx}{\ZCursor{\EEHole}}{\TUnknown}{\ZCursor{\ECMV}}{\TMV}{\AIMV}$.
+      $\ASEActionIter{\ctx}{\ZCCursor{\EEHole}}{\TUnknown}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$.
 
-    \item If $\ctxAnaType{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that
-      $\AAEActionIter{\ctx}{\ZCursor{\EEHole}}{\ZCursor{\ECMV}}{\TMV}{\AIMV}$.
+    \item If $\ctxAnaTypeM{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that
+      $\AAEActionIter{\ctx}{\ZCCursor{\EEHole}}{\ZCCursor{\ECMV}}{\TMV}{\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 $\zWellFormed{\ZMV}$ and $\ctxSynTypeM{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and
-      $\ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV'}{\TMV'}{\AMV}$ and
-      $\ASEActionIter{\ctx}{\ZMV}{\TMV}{\ZMV''}{\TMV''}{\AMV}$, then $\ZMV' = \ZMV''$ and
-      $\equal{\TMV'}{\TMV''}$.
-
-    \item If $\zWellFormed{\ZMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZMV}}{\TMV}$ and
-      $\AAEActionIter{\ctx}{\ZMV}{\ZMV'}{\TMV}{\AMV}$ and
-      $\AAEActionIter{\ctx}{\ZMV}{\ZMV''}{\TMV}{\AMV}$, then $\ZMV' = \ZMV''$.
+    \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$
+        and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$
+      then $\ZTMV' = \ZTMV''$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$
+        and $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV''}{\TMV''}{\AMV}$,
+      then $\ZCMV' = \ZCMV''$
+        and $\equal{\TMV'}{\TMV''}$.
+
+    \item If $\zWellFormed{\ZCMV}$
+        and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$
+        and $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$
+        and $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV''}{\TMV}{\AMV}$,
+      then $\ZCMV' = \ZCMV''$.
   \end{enumerate}
 \end{theorem}