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