simplify let rule

new_system3.tex

@@ -247,20 +247,35 @@ rules, because one branch is already unreachable and retyping only occurs with s
 %   {\Gamma\vdash\lambda x:s.e: t}
 %   { }
 % \\
-\Infer[LetRefine]
+\Infer[LetFirst]
   {
-  x\in\dom\Gamma\Rightarrow t=\Gamma(x)\\x\not\in\dom\Gamma\Rightarrow t=\Any\\
-  x\in\dom\Gamma'\Rightarrow t'=\Gamma'(x)\\x\not\in\dom\Gamma'\Rightarrow t'=\Any\\
   \Gamma\avdash\Gammap\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\
-  \forall i\in I.\ t_i\land t\leq t' \Rightarrow \Gamma_i\subst{x}{t_i\land t}\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : S_i\\
-  \forall i\in I.\ t_i\land t\not\leq t' \Rightarrow\Gamma_i\land\Gamma'\bvdash{a}{t'\land t\land t_i}\{(t_j,\Gamma_j)\}_{j\in J_i}\\
-  \forall i\in I.\ \forall j\in J_i.\ \Gamma_i\subst{x}{t_j}\avdash{\Gammap_j\setminus\{x\}}{[]} \ct[\letexp x a e] : S_j}
+  \forall i\in I.\ \Gamma_i,(x:t_i)\avdash\Gammap\ct\letexp x a e : S_i
+  }
   {
-  \Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup S_i \cup \textstyle\bigcup\bigcup S_j
+  \Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup_{i\in I}S_i
   }
-  { }
+  { x\not\in\dom\Gamma }
+\\
+\Infer[LetNoRefine]
+  {
+  \Gamma\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : S
+  }
+  {
+  \Gamma\avdash\Gammap\ct\letexp x a e : S
+  }
+  { x\in\dom\Gamma \text{ and } (x\not\in\dom\Gammap \text{ or } \Gamma(x)\leq\Gammap(x)) }
+\\
+\Infer[LetRefine]
+  {
+  \Gamma\land\Gammap\bvdash{a}{\Gamma(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\
+  \forall i\in I.\ \Gamma\subst{x}{t_i}\avdash{\Gamma_i\setminus\{x\}}{[]} \ct[\letexp x a e] : S_i}
+  {
+  \Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup_{i\in I} S_i
+  }
+  { x\in\dom\Gamma \text{ and } x\in\dom\Gammap \text{ and } \Gamma(x) \not\leq \Gammap(x) }
 \end{mathpar}
 
-TODO: Check let rule and divide it into simpler rules
+TODO: Check let rule and optimize $\Gammap$ (it should be minimal but it isn't as output of $\bvdash{t}{a}$)
 
 TODO: Abs rules