(\x.\y.\z.xz(yz))(\x.\y.x)(\x.\y.x) Alpha rename: (\x.\y.\z.xz(yz))(\a.\b.a)(\c.\d.c) Substitute (\a.\b.a) for x: (\y.\z.(\a.\b.a)z(yz))(\c.\d.c) Substitute z for a: (\y.\z.(\b.z)(yz))(\c.\d.c) Substitute (yz) for b: (\y.\z.z)(\c.\d.c) Substitute (\c.\d.c) for y: \z.z