From a529976985d41266e1ee13f60e3bc96144da5b15 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Fri, 27 Oct 2023 03:00:06 -0400
Subject: [PATCH] formalism: Move type meet out of premise in MSIf-C

---
 formalism/constraint.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/formalism/constraint.tex b/formalism/constraint.tex
index a0245dd..cfb6469 100644
--- a/formalism/constraint.tex
+++ b/formalism/constraint.tex
@@ -97,9 +97,10 @@ \section{Constraint generation}
   \judgment{
     \anaConstraint{\ctx}{\ECMV_1}{\TBool}{C_1} \\
     \synConstraint{\ctx}{\ECMV_2}{\TMV_1}{C_2} \\
-    \synConstraint{\ctx}{\ECMV_3}{\TMV_2}{C_3}
+    \synConstraint{\ctx}{\ECMV_3}{\TMV_2}{C_3} \\
+    \TMV_3 = \TMeet{\TMV_1}{\TMV_2}
   }{
-    \synConstraint{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMeet{\TMV_1}{\TMV_2}}{C_1 \cup C_2 \cup C_3 \cup \{ \TMV_1 \approx \TMV_2 \}}
+    \synConstraint{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMV_3}{C_1 \cup C_2 \cup C_3 \cup \{ \TMV_1 \approx \TMV_2 \}}
   }{MSIf-C}
 
   \judgment{