Let x0 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Assume H0: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x1).
Assume H1: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x2).
Assume H2: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x3).
Assume H3: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x4).
Assume H4: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x5).
Assume H5: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x6).
Assume H6: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x7).
Assume H7: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x8).
Assume H8: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x9).
Assume H9: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x10).
Assume H10: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x11).
Assume H11: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x12).
Assume H12: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x13).
The subproof is completed by applying H1.