inline LetNoRefine in LetFirst + simplification in LetRefine

new_system3.tex

@@ -250,7 +250,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
 \Infer[LetFirst]
   {
   \Gamma\avdash\Gammap\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\
-  \forall i\in I.\ \Gamma_i,(x:t_i)\avdash\Gammap\ct\letexp x a e : S_i
+  \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_{i\in I}S_i
@@ -268,7 +268,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
 \\
 \Infer[LetRefine]
   {
-  \Gamma\land\Gammap\bvdash{a}{\Gamma(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\
+  \Gamma\bvdash{a}{\Gamma(x)\land\Gammap(x)}\{(t_i,\Gamma_i)\}_{i\in I}\\
   \forall i\in I.\ \Gamma\subst{x}{t_i}\avdash{(\Gammap\land\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