some fixes

new_system3.tex

@@ -131,12 +131,18 @@ The elements of $\Gamma\avdash\Gammap\ct e:t$ mean:
 {\Gamma \avdash\Gammap\ct e : \{(\Empty,\Gamma)\}}
 { }
 \qquad
-  \Infer[Const]
-  { }
-  {\Gamma\avdash\Gammap\ct c: \{(\basic{c},\Gamma)\}}
-  { }
-  \quad
-  \Infer[Var]
+\Infer[NoDef]
+{ x\in\dom\Gammap\setminus\bv(e)\\
+\Gamma\subst{x}{(\Gamma\land\Gammap)(x)} \avdash{\Gammap\setminus\{x\}}{\ct} e : S}
+{\Gamma \avdash\Gammap{\ct} e : S}
+{ }
+\\
+\Infer[Const]
+{ }
+{\Gamma\avdash\Gammap\ct c: \{(\basic{c},\Gamma)\}}
+{ }
+\quad
+\Infer[Var]
 { }
 { \Gamma \avdash\Gammap\ct x: \{(\Gamma(x),\Gamma)\} }
 { x\in\dom\Gamma }
@@ -273,30 +279,22 @@ rules, because one branch is already unreachable and retyping only occurs with s
 
 \begin{mathpar}
   \Infer[Abs]
-    {\Gamma,(x:s)\avdash{\Gammap}{\ct[\letexp{x}{*}{[]}]} e:\{(t_i,\Gamma_i)\}_{i\in I}\\
+    {\Gamma,(x:s)\avdash{\Gammap}{\ct} e:\{(t_i,\Gamma_i)\}_{i\in I}\\
     \forall i\in I.\ J_i=\{j\,\alt\,j\in I\text{ s.t. }
     \forall y\in\fv(e).\ \Gamma_j(y)\leq\Gamma_i(y)\}\\
     \forall i\in I.\ u_i = \bigwedge_{j\in J_i}(\arrow{\Gamma_j(x)}{(
-      t_i\vee\bigvee_{\substack{j\in J_i\text{ s.t. }
-      \Gamma_i(x)\land\Gamma_j(x)\neq\varnothing\\\text{ and }
-      \exists y\in\bv(e).\ \Gamma_j(y)\not\leq\Gamma_i(y)}
-      } t_j
+      t_j\vee\bigvee_{\substack{k\in J_i\text{ s.t. }
+      \Gamma_j(x)\land\Gamma_k(x)\neq\varnothing\\\text{ and }
+      \exists y\in\bv(e).\ \Gamma_k(y)\not\leq\Gamma_j(y)}
+      } t_k
     )})
     }
     {\Gamma\vdash\lambda x:s.e: \{(u_i,\Gamma_i)\,\alt\,i\in I\}}
     { }
 \end{mathpar}
 
-TODO: Check let rule
-
 TODO: Check abs rule
 
-TODO: What if the initial environment already contains some entries?
-Or if a variable is used before being declared?
-Should we add guardians to split rules? ($x\in\bv(\ct)$)
-
-TODO: Add * to grammar and add corresponding rules
-
 \subsection{Backward typing rules}
 
 \begin{mathpar}