times c2 c3
= (\m.\n.\z'. m (n z')) c2 c3
= \z'.c2 (c3 z')
= \z'.c2 {[\s.\z.s (s (s z))] z'}
= \z'.c2 [\z.z' (z' (z' z))]
= \z'.[\s.\z.s (s z)] [\z.z' (z' (z' z))]
= \z'.\z.[\z.z' (z' (z' z))] ([\z.z' (z' (z' z))] z)
= \z'.\z.[\z.z' (z' (z' z))] [z' (z' (z' z))]
= \z'.\z.z' (z' (z' [z' (z' (z' z))]))
= \s.\z.s (s (s (s (s (s z)))))
= c6