From 210a1f87f1c7eedbdff8e83c19c96ebcdaf3cb24 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Mon, 9 Oct 2023 17:25:02 -0400
Subject: [PATCH] formalism: Remove first two prmises from UALetPat

---
 formalism/patterned.tex | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/formalism/patterned.tex b/formalism/patterned.tex
index 8e3ea7a..28605a7 100644
--- 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}
   }{