add some notes/todos

new_system3.tex

@@ -379,15 +379,13 @@ the environment is supposed to already contain a type for $x$.
 TODO: Simplify Case rule: as the expression has been typed before backtyping,
 $x$ is supposed to be included into $t_x$ or $\neg t_x$.
 
-TODO: Improve Abs rule
+TODO: No need to return the type of the expression. The definition will be retyped anyway
+after the splits.
 
-TODO: Is the Inter rule even needed?? (now that result of backtyping must be intersected with the original env)
+TODO: The Inter rule seems to be not needed needed anymore (now that result of backtyping must be intersected with the original env)
 
 TODO: Algorithmic App, Inter and EFQ rule
 
-TODO: Is the Comp rule needed in this new setting where every application is alone in a let,
-and where union-arrow app are backtyped by splitting possibilities?
-
 \subsection{Algorithmic typing rules (alternative attempt)}
 
 \begin{mathpar}