Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

Assume H2: α ∈ PSNo (ordsucc α) (λδ ⇒ δ ∈ x ∧ δ ≠ α).

Set p to be the term λδ ⇒ δ ∈ x ∧ δ ≠ α of type set → prop.

Apply binunionE {β ∈ ordsucc α|p β} {β '|β ∈ ordsucc α, ¬ p β} α H2 to the current goal.

Assume H3: α ∈ {β ∈ ordsucc α|p β}.

Apply SepE2 (ordsucc α) p α H3 to the current goal.

Assume _.

Assume H4: α ≠ α.

Apply H4 to the current goal.

Use reflexivity.

Assume H3: α ∈ {β '|β ∈ ordsucc α, ¬ p β}.

Apply ReplSepE_impred (ordsucc α) (λβ ⇒ ¬ p β) (λx ⇒ x ') α H3 to the current goal.

Let β be given.

Assume Hb: β ∈ ordsucc α.

Assume H4: ¬ p β.

Assume H5: α = β '.

Apply tagged_not_ordinal β to the current goal.

We will prove ordinal (β ').

rewrite the current goal using H5 (from right to left).

We will prove ordinal α.

An exact proof term for the current goal is SNoLev_ordinal x Hx.

∎