Name collisions not handled in β-reduction #2

The term (λx. λy. x y) y should be reduced to λz. y z instead of λy. y y to avoid name collisions.

Image