Let x be given.
Assume Hx.
Apply xm (SNoL x = 0) to the current goal.
Assume H1: SNoL x = 0.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
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.
∎