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