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