add idea for typing lets

refining2.tex

@@ -153,6 +153,11 @@ improves these two points.
 TODO: $\triangleright$ should return a set of environments (mapping variables only) instead
 of a set of types for a given variable?
 
+TODO: typing rule for the let. If we want full control flow, it should compute
+$e_2 \triangleright_y \psi$ and, for all $t$ in $\psi$, type $e_2$ under the hypothesis
+that $e_1$ has type $t$ (and, finally,
+under the hypothesis that $e_1$ has type $\tyof{e_1}{\Gamma}\setminus\bigcup_{t\in\psi}t$).
+
 TODO: The $\evdash e t$ operator is used in the Case, OverApp and OverLet rules,
 but what we would actually need is an operator that computes the other direction:
 which environments can surely lead to $e$ having the type $t$?