Let x0 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H0: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x1).
Assume H1: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x2).
Assume H2: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x3).
Assume H3: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x4).
Assume H4: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x5).
Assume H5: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x6).
Assume H6: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x7).
Assume H7: x0 (λ x1 x2 x3 x4 x5 x6 x7 x8 : (ι → ι) → ι → ι . x8).
The subproof is completed by applying H5.