Help understand beta reduction example I am currently reading a text book on distributed computing systems that includes a short introduction to $\lambda$-calculus. There is an example of evaluating the sequence $(((if \space \space  true) \space \space 4) \space \space 5)$ which is written below. 


*

*$\space\space(((\lambda b.\lambda t.\lambda e.((b \space t) \space e) \space \lambda x.\lambda y.x) \space 4) \space 5) $

*$\space\space((\lambda t.\lambda e ((\lambda x.\lambda y.x \space \space t) \space e) \space 4) \space 5) $

*$\space\space(\lambda e ((\lambda x.\lambda y.x \space \space 4) \space \space e) \space \space 5) $

*$\space\space((\lambda x.\lambda y.x \space \space 4) \space \space 5) $

*$\space\space(\lambda y.4 \space \space 5) $

*$\space\space 4$
The author has used $\beta$-reduction on each line and I can follow up until the second to last reduction. Could someone explain how we get from line 4 to line 6? 

When going from line 4 to line 5, we substitute $x=4$ into $\lambda y. x$, because the inner argument is bound to the $\lambda x$.  The 5 is then passed to the result and bound to the $\lambda y$, so that we substitute $y=5$ into $\lambda y. 4$.  Since $y$ does not appear free in $4$, this does not alter the expression, so we end up with $4$.
