(\f.(\x.f (x x)) (\x.f (x x)))
 \A.\m.\n.(m (\x.\a.\b.a) (\a.\b.b)) 
        (\f.\x.f (n f x))
        ((n (\x.\a.\b.a) (\a.\b.b)) 
          (A (\f.\x.m (\g.\h.h (g f)) (\u.x) (\u.u)) (\a.\b.a b))
          (A
            (\f.\x.m (\g.\h.h (g f)) (\u.x) (\u.u))
            (A
              m
              (\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)))))