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