Let alpha be given.

Assume Ha.

Let x be given.

Assume Hx.

Let p be given.

Assume Hp.

Apply SNoS_E alpha Ha x Hx to the current goal.

Let beta be given.

Assume H1.

Apply H1 to the current goal.

Assume Hb: beta ∈ alpha.

Assume H1: SNo_ beta x.

We prove the intermediate claim Lb: ordinal beta.

An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.

We prove the intermediate claim Lx: SNo x.

An exact proof term for the current goal is SNo_SNo beta Lb x H1.

Apply SNoLev_prop x Lx to the current goal.

Assume Hx1: ordinal (SNoLev x).

Assume Hx2: SNo_ (SNoLev x) x.

We prove the intermediate claim Lxb: SNoLev x = beta.

An exact proof term for the current goal is SNoLev_uniq2 beta Lb x H1.

We prove the intermediate claim Lxa: SNoLev x ∈ alpha.

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

An exact proof term for the current goal is Hb.

An exact proof term for the current goal is Hp Lxa Hx1 Lx Hx2.

∎