λx. (λy. (λz. (? x) (? z)) (? y)) let f(z1,z2,z3) x -> g(h(z1 x, z2), z3) g(z1,z2) y -> z1(z2 y) h(z1,z2) z -> z1(z2 z) in f(n1,n2,n3) λx. (λy. (λz. (n1 x) (n2 z)) (n3 y))