Lambda Calculus: Reducing to Normal Form I'm having trouble understanding how to reduce lambda terms to normal form.  We just got assigned a sheet with a few problems to reduce, and the only helpful thing I've found is the following example in the book:
(λf.λx.f(fx))(λy.y+1)2
->(λx.(λy.y+1)((λy.y+1)x))2 //How'd it get to this??
->(λx.(λy.y+1)(x+1))2
->(λx.(x+1+1))2
->(2+1+1)
I'm pretty sure I understand most of it... except for their first step (everything else is pretty much substitution as if it was: f(x) = x + 3, x = y, therefore y+3)
Can someone please explain this to me? I pretty much have no experience with lambda calculus.
Thanks,
Sean

Basically, the function $(\lambda f.\lambda x.f(fx))$ is applied to the argument $\lambda y.y+1$. This step is also called beta reduction. 
