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