Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Let x1 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 = x1 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x2 = x1 leaving 13 subgoals.
Apply H1 with
λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) = x2 leaving 13 subgoals.
Let x2 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Assume H3: x2 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3).
The subproof is completed by applying H3.
Apply FalseE with
(λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) = λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x3.
Apply neq_1_0.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H2 with λ x3 x4 . x2 x4 x3.
Apply FalseE with
(λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) = λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x4.
Apply neq_2_0.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H2 with λ x3 x4 . x2 x4 x3.
Apply FalseE with
(λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) = λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x5.
Apply neq_3_0.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H2 with λ x3 x4 . x2 x4 x3.