Let n be given.

Assume Hn.

We prove the intermediate claim Ln: nat_p n.

An exact proof term for the current goal is omega_nat_p n Hn.

An exact proof term for the current goal is SNo_SNo (ordsucc n) (ordinal_ordsucc n (nat_p_ordinal n Ln)) (eps_ n) (SNo__eps_ n Hn).

∎