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