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