From "Type Theory and Formal Proof" by Rob Nederpelt and Herman Geuvers:
Definition 2.4.2
(1) A statement is of the form $M : \alpha$, where $M \in \Lambda_{\mathbb{T}}$ and $\sigma \in \mathbb{T}$. In such a statement, $M$ is called the subject and $\alpha$ the type.
(2) A declaration is a statement with a variable as subject.
(3) A context is a list of declarations with different subjects.
Definition 2.4.5 (Derivation rules for $\lambda \to$)
(var) $\Gamma \vdash x : \alpha$ if $x : \alpha \in \Gamma$
(appl) $\Gamma \vdash M : \alpha \to \tau \quad \Gamma \vdash N : \alpha \implies \Gamma \vdash M N : \tau$
(abst) $\Gamma, x : \alpha \vdash M : \tau \implies \Gamma \vdash \lambda x : \alpha . M : \alpha \to \tau$
Definition 2.10.1
(2) Context $\Gamma'$ is a subcontext of context $\Gamma$, or $\Gamma' \subseteq \Gamma$, if all declarations occurring in $\Gamma'$ also occur in $\Gamma$, in the same order.
Lemma 2.10.5
(1) (Thinning) Let $\Gamma'$ and $\Gamma''$ be contexts such that $\Gamma' \subseteq \Gamma''$. If $\Gamma' \vdash M : \alpha$, then also $\Gamma'' \vdash M : \alpha$.
Note: I replaced the horizontal bar between the premisses and conclusion in the derivation rules with $\implies$ since I could not get the bar to typeset as intended.
Suppose I assign the following in Lemma 2.10.5:
$\Gamma' = y : B$
$\Gamma'' = x : C, y : B$
$M = \lambda x : A . y$
$\alpha = A \to B$
Then
$\Gamma' \vdash M : \alpha = y : B \vdash \lambda x : A . y : A \to B$
$\Gamma'' \vdash M : \alpha = x : C, y : B \vdash \lambda x : A . y : A \to B$.
For a derivation of the first I have:
(i) $y : B, x : A \vdash y : B$ (var)
(ii) $y : B \vdash \lambda x : A . y : A \to B$ (abst on i)
I am unable to find a derivation for the second as the lemma implies. Is there a derivation, or am I missing something else?
