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