formalism: Remove first two prmises from UALetPat

hazelgrove · Oct 9, 2023 · b615801 · b615801
1 parent f61ec67
commit b615801
Showing 1 changed file with 2 additions and 6 deletions.
diff --git a/formalism/patterned.tex b/formalism/patterned.tex
@@ -305,9 +305,7 @@ \subsection{Unmarked expressions}
 %
 \begin{mathpar}
   \inferrule[USLetPat]{
-    \ctxSynPatU{\ctx}{\PMV}{\TMV_p} \\
-    \ctxAnaTypeU{\ctx}{\EMV_{1}}{\TMV_p} \\
-    \ctxSynTypeU{\ctx}{\EMV_{1}}{\TMV_{1}} \\\\
+    \ctxSynTypeU{\ctx}{\EMV_{1}}{\TMV_{1}} \\
     \ctxAnaPatU{\ctx}{\PMV}{\TMV_{1}}{\ctx'} \\
     \ctxSynTypeU{\ctx'}{\EMV_{2}}{\TMV_2}
   }{
@@ -325,9 +323,7 @@ \subsection{Unmarked expressions}
   }
 
   \inferrule[UALetPat]{
-    \ctxSynPatU{\ctx}{\PMV}{\TMV_p} \\
-    \ctxAnaTypeU{\ctx}{\EMV_{1}}{\TMV_p} \\
-    \ctxSynTypeU{\ctx}{\EMV_{1}}{\TMV_{1}} \\\\
+    \ctxSynTypeU{\ctx}{\EMV_{1}}{\TMV_{1}} \\
     \ctxAnaPatU{\ctx}{\PMV}{\TMV_{1}}{\ctx'} \\
     \ctxAnaTypeU{\ctx'}{\EMV_{2}}{\TMV_2}
   }{