Let me show the problem on an example...
An actual task from one of the former exams:
Consider a simple functional language:
$$e::= x|n|e_1e_2|\lambda x.e$$
With typing rules:
$$\tau ::= \mathtt{int} | \mathtt{foo} | \tau_1 \rightarrow \tau_2$$
$$\Gamma \vdash n : \mathtt{int}$$
$$\Gamma (x : \tau) \vdash x : \tau$$
$$\begin{array} {c} \Gamma(x : \tau) \vdash e : \rho \\ \hline \Gamma \vdash \lambda x.e : \tau \rightarrow \rho\end{array}$$
$$\begin{array}{c} \Gamma\vdash e_1:\tau\rightarrow \rho\quad\Gamma\vdash e_2:\tau \\ \hline \Gamma\vdash e_1e_2 : \rho\end{array}$$
$$\begin{array}{c}\Gamma\vdash e:\tau \\ \hline \Gamma\vdash e: \mathtt{foo}\end{array}$$
Where the environment $\Gamma$ is a partial function from the set of variables into the set of types and $\Gamma(x:t)$ denotes an environment that assignts the type $t$ to the variable $x$ and works like $\Gamma$ for all other variables.
Derive types for the following expressions:
(omitted for brevity)
Example: Type derivation for $\lambda x.\lambda y.x$:
$$\begin{array}{c}x:\alpha,\;y:\beta\vdash x:\alpha \\ \hline x:\alpha\vdash \lambda y.x:\beta\rightarrow\alpha \\ \hline \vdash\lambda x.\lambda y. x : \alpha \rightarrow (\beta\rightarrow\alpha) \end{array}$$
It is this example that perplexes me. Why is it necessary to put $x:\alpha$ on the left-hand side of $\vdash$ in the second step of the derivation? My thinking is that $\lambda x.y : \beta\rightarrow \alpha$ results from both $x:\alpha$ and $y:\beta$ so there's no reason to put $x:\alpha$ on the lhs of $\vdash$ but not $y:\beta$.
But $\begin{array}{c}x:\alpha,\;y:\beta\vdash x:\alpha,\; y:\beta \\ \hline x:\alpha,\; y:\beta\vdash \lambda y.x:\beta\rightarrow\alpha \end{array}$ is a tautology that brings in nothing, so we should instead simplify this to $\begin{array}{c}x:\alpha,\;y:\beta \\ \hline \vdash \lambda y.x:\beta\rightarrow\alpha \end{array}$. Note that this is precisely what the third step of derivation seems to be doing: $\begin{array}{c} x:\alpha\vdash \lambda y.x:\beta\rightarrow\alpha \\ \hline \vdash\lambda x.\lambda y. x : \alpha \rightarrow (\beta\rightarrow\alpha) \end{array}$ They simply put nothing on the left-hand side of the $\vdash$.
What am I missing here? Is this related to the form of the axiom that seems to be used here - $\begin{array} {c} \Gamma(x : \tau) \vdash e : \rho \\ \hline \Gamma \vdash \lambda x.e : \tau \rightarrow \rho\end{array}$ - where the environment used above the vertical line contains the assignment $x:\tau$ while the environment used below the vertical line is devoid of this assignment? Which is why in $x:\alpha\vdash \lambda y.x:\beta\rightarrow\alpha$ the assignment $x:\alpha$ must be present before the $\vdash$, but the assignment $y:\beta$ must not? Is my reasoning correct? But if it is, then why does the third step seem to differ and is of the form $\vdash\lambda x.\lambda y. x : \alpha \rightarrow (\beta\rightarrow\alpha)$ and not $\lambda y.x : \beta\rightarrow\alpha \vdash\lambda x.\lambda y. x : \alpha \rightarrow (\beta\rightarrow\alpha)$?
Or am I splitting hairs here? But my thinking is that I'm not certain what degree of accuratness is required by this professor so I wouldn't like to loose points on something of this sort... Could you clear my confusion?