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