Let x0 of type ι → (ι → ο) → ο be given.
Assume H1:
∀ x1 x2 . ∀ x3 x4 : ι → ο . x0 x1 x3 ⟶ x0 x2 x4 ⟶ x0 (a3eb9.. x1 x2) (c0709.. x3 x4).
Assume H2:
∀ x1 x2 . ∀ x3 x4 : ι → ο . x0 x1 x3 ⟶ x0 x2 x4 ⟶ x0 (bf68c.. x1 x2) (6e020.. x3 x4).
The subproof is completed by applying H0.