Assume H1: SNoL x ≠ 0.
Apply orIR to the current goal.
We prove the intermediate
claim L1:
∀y ∈ SNoL x, SNo y.
Let y be given.
Assume Hy.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume _ _ Hx3 _.
Apply SNoL_E x Hx3 y Hy to the current goal.
Assume H _ _.
An exact proof term for the current goal is H.
An
exact proof term for the current goal is
finite_max_exists (SNoL x) L1 (SNoS_omega_SNoL_finite x Hx) H1.