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 SNoLev_uniq2 alpha La (x ∩ SNoElts_ alpha) L1.
∎