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