Let α be given.

Assume Ha.

Let x be given.

Assume Hx.

Let p be given.

Assume Hp.

Apply SNoS_E α Ha x Hx to the current goal.

Let β be given.

Assume H1.

Apply H1 to the current goal.

Assume Hb: β ∈ α.

Assume H1: SNo_ β x.

We prove the intermediate claim Lb: ordinal β.

An exact proof term for the current goal is ordinal_Hered α Ha β Hb.

We prove the intermediate claim Lx: SNo x.

An exact proof term for the current goal is SNo_SNo β 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 = β.

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

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

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.

∎