diff --git a/formalism/typed.tex b/formalism/typed.tex
index bc07c7e..ab04484 100644
--- a/formalism/typed.tex
+++ b/formalism/typed.tex
@@ -707,10 +707,10 @@ \subsubsection{Synthetic expression actions}
 
   \inferrule[ASEZipApL3]{
     \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\
+    \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\
     \notMatchedArrow{\TMV_1'}
   }{
-    \ASEAction{\ctx}{\ZCApL{\ZCMV_1}{\ECMV_2}}{\TMV}{\ZCApL{\ECInconType{\ZCMV_1'}}{\ECMV_2}}{\TUnknown}{\AMV}
+    \ASEAction{\ctx}{\ZCApL{\ZCMV_1}{\ECMV_2}}{\TMV}{\ZCApSynNonMatchedArrowL{\ZCMV_1'}{\ECMV_2}}{\TUnknown}{\AMV}
   }
 
   \inferrule[ASEZipApL4]{
@@ -739,7 +739,7 @@ \subsubsection{Synthetic expression actions}
     \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}{\ZCMV_2}{\ZCMV_2'}{\TMV_2}{\AMV}
@@ -747,10 +747,16 @@ \subsubsection{Synthetic expression actions}
     \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{\ZCMV_1}}{\TMV_1} \\
     \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\
-    \consistent{\TMV_1}{\TMV_1'}
+    \equal{\TMV_1}{\TMV_1'}
   }{
     \ASEAction{\ctx}{\ZCLetL{x}{\ZCMV_1}{\ECMV_2}}{\TMV_2}{\ZCLetL{x}{\ZCMV_1'}{\ECMV_2}}{\TMV_2}{\AMV}
   }
@@ -758,7 +764,7 @@ \subsubsection{Synthetic expression actions}
   \inferrule[ASEZipLetL2]{
     \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV_1}}{\TMV_1} \\
     \ASEAction{\ctx}{\ZCMV_1}{\TMV_1}{\ZCMV_1'}{\TMV_1'}{\AMV} \\\\
-    \inconsistent{\TMV_1}{\TMV_1'} \\
+    \notEqual{\TMV_1}{\TMV_1'} \\
     \ctxSynFixedInto{\extendCtx{\ctx}{x}{\TMV_1'}}{\erase{\ECMV_2}}{\ECMV_2'}{\TMV_2'}
   }{
     \ASEAction{\ctx}{\ZCLetL{x}{\ZCMV_1}{\ECMV_2}}{\TMV_2}{\ZCLetL{x}{\ZCMV_1'}{\ECMV_2'}}{\TMV_2'}{\AMV}
@@ -863,6 +869,74 @@ \subsubsection{Synthetic expression actions}
   }{
     \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}