Let x0 of type ι be given.

Let x1 of type ι be given.

Apply unknownprop_b1688df6c44ba77d79de73f8f342bb066cd3f42d8bb655e89687f3927126b720 with λ x2 x3 : ι → ι → ο . PNoLt (SNoLev x0) (λ x4 . In x4 x0) (SNoLev x1) (λ x4 . In x4 x1) ⟶ x3 x0 x1.

Assume H0: PNoLt (SNoLev x0) (λ x2 . In x2 x0) (SNoLev x1) (λ x2 . In x2 x1).

The subproof is completed by applying H0.

■

Proofgold Proof