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