Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: SNo x0. Assume H1: SNoLev x0 = x0. Claim L2: ordinal x0 Apply H1 with λ x1 x2 . ordinal x1. Apply SNoLev_ordinal with x0. The subproof is completed by applying H0. Apply ordinal_SNoR with x0. The subproof is completed by applying L2. ■