I am going over the proofs for the simply typed lambda calculus in the book "Types and Programming languages" by Benjamin Pierce. I am trying to find inspiration for the similar proofs for System F Omega. When I was going over the preservation under substitution proof I was a bit puzzled.

The hypothesis of the proof is:

If $\Gamma ,x:S \vdash t:T $ and $\Gamma \vdash s:S$ then $\Gamma \vdash [x \mapsto s]t : T$

So far I understand the proof quite well, but for the case $T-Abs$ I'm a bit lost. The rule is shown below.

$$ \dfrac{\Gamma ,x:T_1 \vdash t_2 : T_2} {\Gamma \vdash \lambda x:T_1 . t_2 : T_1 \rightarrow T_2} $$

To prove the hypothesis for this case we use the previously proven lemmas weakening and permutation.

We assume that in this proof $x \neq y$ and $y \notin FV(s)$.

First we list the givens:

1. $t = \lambda y:T_2 . t_1$
2. $ T = T_1 \rightarrow T_2$
3. The first subderivation: $\Gamma ,x:S,y:T_2 \vdash t_1 : T_2$
4. The second subderivation: $\Gamma \vdash s:S$ by hypothesis.

Step 1 The first step we take is using permutation on the first sub-derivation, yielding: $\Gamma ,y:T_2,x:S \vdash t_1 : T_2$. The reason why this happens is a bit unclear to me. I am assuming that the actual order of the extensions of $\Gamma$ matter for the third step.

Step 2 The second step, which is the one that is unclear to me, is applying weakening to the second sub-derivation: changing $\Gamma \vdash s:S$ into $\Gamma ,y:T_2\vdash s:S$. The reason that I find this odd is that this new form of the sub-derivation is not used anywhere in the proof.

Step 3: By the induction of our hypothesis we know that $\Gamma ,x:S,y:T_2 \vdash t_1 : T_2$ implies $\Gamma ,y:T_2 \vdash [x \mapsto s]t_1 : T_2$. And since we know that, we can apply the $T-Abs$ rule. Since that is what it basically says. We wrap the given sub-derivation in a lambda and we have to remove the $y:T_2$ from the context because it is now introduced by the abstraction we constructed:

$$\Gamma \vdash \lambda y:T_2 . [x \mapsto s]t_1 : T_1 \rightarrow T_2$$

And finally we can move the substitution outside because we assumed that $x \neq y$ and $y \notin FV(s)$.

$$\Gamma \vdash [x \mapsto s]\lambda y:T_2 . t_1 : T_1 \rightarrow T_2$$

And this is exactly what we had to prove.

The problem I have with the second sub-derivation is that we nowhere in the prove actually used it. We never relied on that fact. Any input would be highly appreciated.

I am going over the proofs for the simply typed lambda calculus in the book "Types and Programming languages" by Benjamin Pierce. I am trying to find inspiration for the similar proofs for System F Omega. When I was going over the preservation under substitution proof for the simply typed lambda calculus I was a bit puzzled.

The hypothesis of the proof is:

If $\Gamma ,x:S \vdash t:T $ and $\Gamma \vdash s:S$ then $\Gamma \vdash [x \mapsto s]t : T$

So far I understand the proof quite well, but for the case $T-Abs$ I'm a bit lost. The rule is shown below.

$$ \dfrac{\Gamma ,x:T_1 \vdash t_2 : T_2} {\Gamma \vdash \lambda x:T_1 . t_2 : T_1 \rightarrow T_2} $$

To prove the hypothesis for this case we use the previously proven lemmas weakening and permutation.

We assume that in this proof $x \neq y$ and $y \notin FV(s)$.

First we list the givens:

1. $t = \lambda y:T_2 . t_1$
2. $ T = T_1 \rightarrow T_2$
3. The first subderivation: $\Gamma ,x:S,y:T_2 \vdash t_1 : T_2$
4. The second subderivation: $\Gamma \vdash s:S$ by hypothesis.

Step 1 The first step we take is using permutation on the first sub-derivation, yielding: $\Gamma ,y:T_2,x:S \vdash t_1 : T_2$. The reason why this happens is a bit unclear to me. I am assuming that the actual order of the extensions of $\Gamma$ matter for the third step.

Step 2 The second step, which is the one that is unclear to me, is applying weakening to the second sub-derivation: changing $\Gamma \vdash s:S$ into $\Gamma ,y:T_2\vdash s:S$. The reason that I find this odd is that this new form of the sub-derivation is not used anywhere in the proof.

Step 3: By the induction of our hypothesis we know that $\Gamma ,x:S,y:T_2 \vdash t_1 : T_2$ implies $\Gamma ,y:T_2 \vdash [x \mapsto s]t_1 : T_2$. And since we know that, we can apply the $T-Abs$ rule. Since that is what it basically says. We wrap the given sub-derivation in a lambda and we have to remove the $y:T_2$ from the context because it is now introduced by the abstraction we constructed:

$$\Gamma \vdash \lambda y:T_2 . [x \mapsto s]t_1 : T_1 \rightarrow T_2$$

And finally we can move the substitution outside because we assumed that $x \neq y$ and $y \notin FV(s)$.

$$\Gamma \vdash [x \mapsto s]\lambda y:T_2 . t_1 : T_1 \rightarrow T_2$$

And this is exactly what we had to prove.

The problem I have with the second sub-derivation is that we nowhere in the prove actually used it. We never relied on that fact. Any input would be highly appreciated.