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.