Actually, now that I'm reading the term, I'm a little surprised by the notation λsz.s(z). I think it is more conventionally written λsz.s z (and similarly in ML

Actually, now that I'm reading the term, I'm a little surprised by the notation λsz.s(z). I think it is more conventionally written λsz.s z (and similarly in ML: fun s z -> s z). If you write it without syntax simplification, it is (λs.(λz.(s z))). Then, you usually write only one lambda as it can be seen as function with two arguments (λsz.(s z)). Then you remove the most outside parenthesis: λsz.(s z). Since abstraction has lower precedence that application, you can finally write it λsz.s z. An important thing to know is that in functional langages (lambda calculus, lisp or ML), application is written (f x) - and not f(x) - and is left associative, so (f x) y is written f x y.