Let x be given.

Assume Hx.

Let α be given.

Assume Ha.

We prove the intermediate claim La: ordinal α.

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

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

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

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

∎