(\True.\False.\Pair.\Y.(\Succ.Y Succ) (\n.Pair False n)) (\x.\y.x) (\x.\y.y) (\x.\y.\z.z x y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\False.\Pair.\Y.(\Succ.Y Succ) (\n.Pair False n)) (\x.\y.y) (\x.\y.\z.z x y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Pair.\Y.(\Succ.Y Succ) (\n.Pair (\x.\y.y) n)) (\x.\y.\z.z x y) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Y.(\Succ.Y Succ) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)) (\f.(\x.f (x x)) (\x.f (x x)))
 -> (\Succ.(\f.(\x.f (x x)) (\x.f (x x))) Succ) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)
 -> (\f.(\x.f (x x)) (\x.f (x x))) (\n.(\x.\y.\z.z x y) (\x.\y.y) n)
 -> (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)) (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x))
 -> (\n.(\x.\y.\z.z x y) (\x.\y.y) n) ((\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)) (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)))
 -> (\x.\y.\z.z x y) (\x.\y.y) ((\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)) (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)))
 -> (\y.\z.z (\x.\y.y) y) ((\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)) (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)))
 -> \z.z (\x.\y.y) ((\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)) (\x.(\n.(\x.\y.\z.z x y) (\x.\y.y) n) (x x)))
END
