Let x0 of type (ι → ο) → ο be given.
Let x1 of type (ι → ι → ο) → ο be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Let x9 of type ι be given.
Let x10 of type ι be given.
Let x11 of type ι be given.
Assume H0: ∀ x12 : ι → ο . x12 x2 ⟶ x12 x3 ⟶ x12 x4 ⟶ x12 x5 ⟶ x12 x6 ⟶ x12 x7 ⟶ x12 x8 ⟶ x12 x9 ⟶ x12 x10 ⟶ x12 x11 ⟶ x0 x12.
Assume H1: ∀ x12 : ι → ι → ο . ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ x12 x4 x11 ⟶ x12 x5 x2 ⟶ x12 x5 x3 ⟶ x12 x5 x4 ⟶ x12 x5 x5 ⟶ x12 x5 x6 ⟶ x12 x5 x7 ⟶ x12 x5 x8 ⟶ x12 x5 x9 ⟶ x12 x5 x10 ⟶ x12 x5 x11 ⟶ x12 x6 x2 ⟶ x12 x6 x3 ⟶ x12 x6 x4 ⟶ x12 x6 x5 ⟶ x12 x6 x6 ⟶ x12 x6 x7 ⟶ x12 x6 x8 ⟶ x12 x6 x9 ⟶ x12 x6 x10 ⟶ x12 x6 x11 ⟶ x12 x7 x2 ⟶ x12 x7 x3 ⟶ x12 x7 x4 ⟶ x12 x7 x5 ⟶ x12 x7 x6 ⟶ x12 x7 x7 ⟶ x12 x7 x8 ⟶ x12 x7 x9 ⟶ x12 x7 x10 ⟶ x12 x7 x11 ⟶ x12 x8 x2 ⟶ x12 x8 x3 ⟶ x12 x8 x4 ⟶ x12 x8 x5 ⟶ x12 x8 x6 ⟶ x12 x8 x7 ⟶ x12 x8 x8 ⟶ x12 x8 x9 ⟶ x12 x8 x10 ⟶ x12 x8 x11 ⟶ x12 x9 x2 ⟶ x12 x9 x3 ⟶ x12 x9 x4 ⟶ x12 x9 x5 ⟶ x12 x9 x6 ⟶ x12 x9 x7 ⟶ x12 x9 x8 ⟶ x12 x9 x9 ⟶ x12 x9 x10 ⟶ x12 x9 x11 ⟶ x12 x10 x2 ⟶ x12 x10 x3 ⟶ x12 x10 x4 ⟶ x12 x10 x5 ⟶ x12 x10 x6 ⟶ x12 x10 x7 ⟶ x12 x10 x8 ⟶ x12 x10 x9 ⟶ x12 x10 x10 ⟶ x12 x10 x11 ⟶ x12 x11 x2 ⟶ x12 x11 x3 ⟶ x12 x11 x4 ⟶ x12 x11 x5 ⟶ x12 x11 x6 ⟶ x12 x11 x7 ⟶ x12 x11 x8 ⟶ x12 x11 x9 ⟶ x12 x11 x10 ⟶ x12 x11 x11 ⟶ x0 (λ x13 . x0 (λ x14 . x12 x13 x14)).