The substitution lemma in lambda-calculus is proved by the following way, but I just did not understand the application of induction hypothesis in it.
The lemma as shown below, where $x$ and $y$ are distinct and $x$ is not among the free variables of $L$:
M[x:=N][y:=L] equals M[y:=L][x:=N[y:=L]]
to prove that in the case where $M= \lambda z.M_1$, by the variable convention, $z$ is distinct from $x$ and $y$, and $z$ is not among the free variables of $N$ and $L$. and The proof goes like this
(1) = (λz.M1)[ x:=N ] [ y:=L ] (2) = λz.M1[ x:=N ] [ y:=L ] by susbtitution definition (3) = λz.M1[ y:=L ] [ x:=N [ y:=L ] ] by induction hypothesis (4) = (λz.M1)[ y:=L ] [ x:=N [ y:=L ] ] by susbtitution definition
so, it is proved.
I think 3th line is obtained by substitution definitions $(M_1 M_2)[x:=N] = (M_1[x:=N])(M_2[x:=N])$, right? Just did not see last line, how it is obtained? how induction hypothesis is applied? substitution lemma given here Can someone explain this point to me? Thanks in advance!