Let x be given.

Assume Hx.

Let alpha be given.

Assume Ha.

We prove the intermediate claim La: ordinal alpha.

An exact proof term for the current goal is ordinal_Hered (SNoLev x) (SNoLev_ordinal x Hx) alpha Ha.

We prove the intermediate claim L1: SNo_ alpha (x ∩ SNoElts_ alpha).

An exact proof term for the current goal is restr_SNo_ x Hx alpha Ha.

An exact proof term for the current goal is SNo_SNo alpha La (x ∩ SNoElts_ alpha) L1.

∎