I am currently trying to read up on type theory and have some quick questions on terminology.
In the following rule,
$$ \frac{x:T_1 \vdash t_2 : T_2}{\vdash \lambda x:T_1.t_2:T_1\to T_2} $$
How would you write that in English? Would the following be correct?
If we have established that under the assumption that $x$ has type $T_1$, $t_2$ has type $T_2$; then we can derive that under the empty set of assumptions, $\lambda x.t_2$ has type $T_1\to T_2$.
Is this just a shorthand for the following?
$$ \frac{\Gamma,x:T_1 \vdash t_2 : T_2}{\Gamma\vdash \lambda x:T_1.t_2:T_1\to T_2} $$
Would this be read as If we have established that under the assumptions of the type environment $\Gamma$ and the binding $x:T_1$, that $t_2$ has type $T_2$; then [$\ldots$]?