# Thinning lemma in simply typed lambda calculus

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?

## 1 Answer

This may just be a consequence of Convention 1.7.2 From now on, we identify α-convertible λ-terms.