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