Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo x0.
Claim L1: ordinal (SNoLev x0)
Apply SNoLev_ordinal with x0.
The subproof is completed by applying H0.
Claim L2: ordinal (ordsucc (SNoLev x0))
Apply ordinal_ordsucc with SNoLev x0.
The subproof is completed by applying L1.
Claim L3: x0 ∈ SNoS_ (ordsucc (SNoLev x0))
Apply SNoS_SNoLev with x0.
The subproof is completed by applying H0.
Apply minus_SNo_Lev_lem1 with ordsucc (SNoLev x0), x0 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
■