Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . bb6a5.. x1 x1 = λ x2 x3 . x3 leaving 17 subgoals.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x3) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x3)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x4) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x4)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x5) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x5)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x6) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x6)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x7) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x7)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x8) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x8)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x9) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x9)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x10) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x10)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x11) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x11)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x12) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x12)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x13) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x13)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x14) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x14)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x15) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x15)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x16) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x16)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x17) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x17)) (λ x2 x3 . x3).
The subproof is completed by applying H1.
Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H1:
x1 (bb6a5.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x18) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x18)) (λ x2 x3 . x3).
The subproof is completed by applying H1.