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