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