Let x be given.
Assume Hx: SNo x.
Set alpha to be the term SNoLev x.
Assume H2: alpha ∈ PSNo (ordsucc alpha) (λdelta ⇒ delta ∈ x ∧ delta ≠ alpha).
Set p to be the term λdelta ⇒ delta ∈ x ∧ delta ≠ alpha of type set → prop.
Apply binunionE {beta ∈ ordsucc alpha|p beta} {beta '|beta ∈ ordsucc alpha, ¬ p beta} alpha H2 to the current goal.
Assume H3: alpha ∈ {beta ∈ ordsucc alpha|p beta}.
Apply SepE2 (ordsucc alpha) p alpha H3 to the current goal.
Assume _.
Assume H4: alpha ≠ alpha.
Apply H4 to the current goal.
Use reflexivity.
Assume H3: alpha ∈ {beta '|beta ∈ ordsucc alpha, ¬ p beta}.
Apply ReplSepE_impred (ordsucc alpha) (λbeta ⇒ ¬ p beta) (λx ⇒ x ') alpha H3 to the current goal.
Let beta be given.
Assume Hb: beta ∈ ordsucc alpha.
Assume H4: ¬ p beta.
Assume H5: alpha = beta '.
Apply tagged_not_ordinal beta to the current goal.
We will prove ordinal (beta ').
rewrite the current goal using H5 (from right to left).
We will prove ordinal alpha.
An exact proof term for the current goal is SNoLev_ordinal x Hx.
∎