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