Let x0 of type (ι → ι) → ι → ι be given.
Let x1 of type ((ι → ι) → ι → ι) → ο be given.
Assume H1: x1 (λ x2 : ι → ι . λ x3 . x3).
Assume H2: ∀ x2 : (ι → ι) → ι → ι . x1 x2 ⟶ x1 (λ x3 : ι → ι . λ x4 . x3 (x2 x3 x4)).
Apply H2 with
x0.
Apply H0 with
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.