Let x0 of type ι be given.

Let x1 of type ι be given.

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

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

The subproof is completed by applying H0.

■

Proofgold Proof