formalism: Fix AEZipProjL and AEZipProjR

hazelgrove · Oct 9, 2023 · 13c28f1 · 13c28f1
1 parent de0512e
commit 13c28f1
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/formalism/untyped.tex b/formalism/untyped.tex
@@ -590,13 +590,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}