Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Assume H0: SNoLt x0 x1. Apply PNoLeI1 with SNoLev x0, SNoLev x1, λ x2 . x2 ∈ x0, λ x2 . x2 ∈ x1. The subproof is completed by applying H0. ■