I am going through Lemma 1.2.11 of "Lectures on the Curry-Howard Isomorphism" by Morten Heine Sørensen and Pawel Urzyczyn. There is a free sample that includes this lemma here: https://play.google.com/store/books/details?id=_mtnm-9KtbEC
1.2.11 Lemma. If $M =_{\alpha} M'$ and $N =_{\alpha} N'$ then $M [ x := N ] =_{\alpha} M' [ x := N' ]$, provided that both sides are defined.
PROOF. By induction on the definition of $M =_{\alpha} M'$. If $M = M'$ then proceed by induction on $M$. The only other interesting case is when we have $M = \lambda z P$ and $M' = \lambda y . P [ z := y ]$, where $y \notin FV ( P )$, and $P [ z := y ]$ is defined. If $x = z$, then $x \notin FV ( M ) = FV ( M' )$ by Lemma 1.2.10. Hence $M [ x := N ] = M =_{\alpha} M' = M' [ x := N' ]$ by Lemma 1.2.5. The case $x = y$ is similar. So assume $x \notin \{ y, z \}$. Since $M [ x := N ]$ is defined, $x \notin FV ( P )$ or $z \notin FV ( N )$. In the former case $M [ x := N ] = \lambda z P$ and $x \notin FV ( P [ z := y ] )$, so $M' [ x := N' ] = \lambda y . P [ z := y ] =_{\alpha} \lambda z . P$.
It remains to consider the case when $x \in FV ( P )$ and $z \notin FV ( N )$. Since $M' [ x := N' ] = ( \lambda y . P [ z := y ] ) [ x := N' ]$ is defined, we have $y \notin FV ( N' )$, and thus also $y \notin FV ( P [ x := N' ] )$. By Lemma 1.2.6 it then follows that $M' [ x := N' ] = \lambda y . P [ z := y ] [ x := N' ] = \lambda y . P [ x := N' ] [ z := y ] =_{\alpha} [ z . P [ x := N' ]$. By the induction hypothesis $\lambda z . P [ x := N' ] =_{\alpha} \lambda z . P [ x := N ] = M [ x := N ]$.
I believe that $[ z . P [ x := N' ]$ is a misprint of $\lambda z . P [ x := N' ]$.
Referenced lemmas:
1.2.5. Lemma.
(i) If $x \notin FV ( M )$ then $M [ x := N ]$ is defined, and $M [ x := N ] = M$.
(ii) If $M [ x := N ]$ is defined then $y \in FV ( M [ x := N ] )$ if and only if either $y \in FV ( M )$ and $x \neq y$ or both $y \in FV ( N )$ and $x \in FV ( M )$.
(iii) The substitution $M [ x := x ]$ is defined and $M [ x := x ] = M$.
(iv) If $M [ x := y ]$ is defined, then $M [ x := y ]$ is of the same length as $M$.
1.2.6 Lemma. Assume that $M [ x := N ]$ is defined, and both $N [ y := L ]$ and $M [ x := N ] [ y := L ]$ are defined, where $x \neq y$. If $x \notin FV ( L )$ or $y \notin FV ( M )$ then $M [ y := L ]$ is defined, $M [ y := L ] [ x := N [ y := L ] ]$ is defined, and $M [ x := N ] [ y := L ] = M [ y := L ] [ x := N [ y := L ] ]$.
1.2.10 Lemma. If $M =_{\alpha} N$ then $FV ( M ) = FV ( N )$.
Substitution is defined as in this question: Formal definition of substitution being defined in type free lambda calculus
Alpha conversion is defined as:
The relation $=_{\alpha}$ ($\alpha$-conversion) is the least (i.e. smallest) transitive and reflexive relation on $\Lambda^{-}$ satisfying the following.
If $y \notin FV ( M )$ and $M [ x := y ]$ is defined then $\lambda x M =_{\alpha} \lambda y . M [ x := y ]$.
If $M =_{\alpha} N$ then $\lambda x M =_{\alpha} \lambda x N$, for all variables $x$.
If $M =_{\alpha} N$ then $MZ =_{\alpha} NZ$.
If $M =_{\alpha} N$ then $ZM =_{\alpha} ZN$.
I think that the case in question can be stated as:
H1. Let $P \in \Lambda^{-}$.
H2. Let $y$ be any variable.
H3. Let $z$ be any variable.
H4. Let $y \notin FV ( P )$.
H5. Let $P [ z := y ]$ be defined.
H6. Let $x$ be any variable.
H7. Let $N \in \Lambda^{-}$.
H8. Let $N' \in \Lambda^{-}$.
H9. Let $N =_{\alpha} N'$.
H10. Let $( \lambda z . P ) [ x := N ]$ be defined.
H11. Let $( \lambda y. P [ z := y ] ) [ x := N' ]$ be defined.
Prove: $( \lambda z . P ) [ x := N ] =_{\alpha} ( \lambda y. P [ z := y ] ) [ x := N']$.
If this is the case then I have:
T1. $( \lambda z . P ) =_{\alpha} ( \lambda y. P [ z := y ] )$ by H1 - H5 and the definition of $\alpha$-conversion.
T2. $FV ( ( \lambda z . P ) ) = FV ( ( \lambda y. P [ z := y ] ) )$ by T1 and Lemma 1.2.10.
T3. $FV ( N ) = FV ( N' )$ by H9 and Lemma 1.2.10.
A1. Let $x = z$.
A1-T1. $z \notin FV ( P ) - \{ z \}$.
A1-T2. $FV ( P ) - \{ z \} = FV ( ( \lambda z . P ) )$.
A1-T3. $x \notin FV ( ( \lambda z . P ) )$ by A1, A1-T1, and A1-T2.
A1-T4. $x \notin FV ( ( \lambda y . P [ z := y ] ) )$ by A1-T3 and T2.
A1-T5. $( \lambda z . P ) [ x := N ] = ( \lambda z . P )$ by A1-T3 and Lemma 1.2.5 (i).
A1-T6. $( \lambda y. P [ z := y ] ) [ x := N' ] = ( \lambda y. P [ z := y ] )$ by A1-T4 and Lemma 1.2.5 (i).
A1-T7. $( \lambda z . P ) [ x := N ] =_{\alpha} ( \lambda y. P [ z := y ] ) [ x := N' ]$ by T1, A1-T5, and A1-T6.
A2. Let $x = y$.
A2-T1. $y \notin FV ( P [ z := y ] ) - \{ y \}$.
A2-T2. $FV ( P [ z := y ] ) - \{ y \} = FV ( ( \lambda y . P [ z := y ] ) )$.
A2-T3. $x \notin FV ( ( \lambda y . P [ z := y ] ) )$ by A2, A2-T1, and A2-T2.
A2-T4. $x \notin FV ( ( \lambda z . P ) )$ by A2-T3 and T2.
A2-T5. $( \lambda y. P [ z := y ] ) [ x := N' ] = ( \lambda y. P [ z := y ] )$ by A2-T3 and Lemma 1.2.5 (i).
A2-T6. $( \lambda z . P ) [ x := N ] = ( \lambda z . P )$ by A2-T4 and Lemma 1.2.5 (i).
A2-T7. $( \lambda z . P ) [ x := N ] =_{\alpha} ( \lambda y. P [ z := y ] ) [ x := N' ]$ by T1, A2-T5, and A2-T6.
A3. Let $x \neq y$ and $x \neq z$.
A3-T1. $x \neq y$ by A3.
A3-T2. $x \neq z$ by A3.
A3-T3. $P [ x := N ]$ is defined by H10, A3-T2, and (e) of the definition of substitution.
A3-T4. $( \lambda z . P ) [ x := N ] = ( \lambda z . P [ x := N ] )$ by H10, A3-T2, and (e) of the definition of substitution.
A3-T5. $x \notin FV ( P )$ or $z \notin FV ( N )$ by H10, A3-T2, and (e) of the definition of substitution.
A3-T6. $P [ z := y ] [ x := N' ]$ is defined by H11, A3-T1, and (e) of the definition of substitution.
A3-T7. $( \lambda y . P [ z := y ] ) [ x := N' ] = ( \lambda y . P [ z := y ] [ x := N' ] )$ by H11, A3-T1, and (e) of the definition of substitution.
A3-T8. $x \notin FV ( P [ z := y ] )$ or $y \notin FV ( N' )$ by H11, A3-T1, and (e) of the definition of substitution.
A3-A4. Let $x \notin FV ( P )$.
A3-A4-T1. $P [ x := N ] = P$ by A3-A4 and Lemma 1.2.5 (i).
A3-A4-T2. $( \lambda z . P [ x := N ] ) = ( \lambda z . P )$ by A3-A4-T1.
A3-A4-T3. $x \notin FV ( y )$ by A3-T1.
A3-A4-T4. $x \notin FV ( P [ z := y ] )$ by H5, A3-A4, A3-A4-T3, and Lemma 1.2.5 (ii).
A3-A4-T5. $P [ z := y ] [ x := N' ] = P [ z := y ]$ by A3-A4-T4 and Lemma 1.2.5 (i).
A3-A4-T6. $( \lambda y. P [ z := y ] [ x := N' ] ) = ( \lambda y . P [ z := y ] )$ by A3-A4-T5.
A3-A4-T7. $( \lambda y. P [ z := y ] ) [ x := N' ] = ( \lambda y . P [ z := y ] )$ by A3-T7 and A3-A4-T6.
A3-A4-T8. $( \lambda z . P ) [ x := N ] =_{\alpha} ( \lambda y. P [ z := y ] ) [ x := N' ]$ by A3-T4, A3-A4-T2, T1, and A3-A4-T7.
A3-A5. Let $x \in FV ( P )$.
A3-A5-T1. $z \notin FV ( N )$ by A3-A5 and A3-T5.
A3-A5-T2. $x \in FV ( P [ z := y ] )$ by H5, A3-A5, A3-T2, and Lemma 1.2.5 (ii).
A3-A5-T2. $y \notin FV ( N' )$ by A3-T8 and A3-A5-T2.
I do not understand the remaining part of the proof. It consists of:
and thus also $y \notin FV ( P [ x := N' ] )$. By Lemma 1.2.6 it then follows that $M' [ x := N' ] = \lambda y . P [ z := y ] [ x := N' ] = \lambda y . P [ x := N' ] [ z := y ] =_{\alpha} [ z . P [ x := N' ]$. By the induction hypothesis $\lambda z . P [ x := N' ] =_{\alpha} \lambda z . P [ x := N ] = M [ x := N ]$.
Is there a further induction on $P$ at this point?