(λx.(λy.((λf.((λh.(h(λp.(h(λq.q)))))
              (λl.(((f(λn.(l n))) x) y))))
         (λg.(λu.(λv.((g u) (g v))))))))