Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: SNo x0. Apply andE with ordinal (SNoLev x0), SNo_ (SNoLev x0) x0. Apply unknownprop_57fda5724944921bc8bfd63237eeffb6555b6cf5fee93ed58eb6cdda96377079 with x0. The subproof is completed by applying H0. ■