Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
Apply SNoS_E2 ω omega_ordinal y Hy to the current goal.
Assume Hy2: ordinal (SNoLev y).
Assume Hy3: SNo y.
Assume Hy4: SNo_ (SNoLev y) y.
Apply SNoS_I ω omega_ordinal (x + y) (SNoLev (x + y)) to the current goal.
We will
prove SNoLev (x + y) ∈ ω.
We prove the intermediate
claim LLxy:
ordinal (SNoLev (x + y)).
Apply SNoLev_ordinal to the current goal.
An
exact proof term for the current goal is
SNo_add_SNo x y Hx3 Hy3.
Apply ordinal_In_Or_Subq (SNoLev (x + y)) ω LLxy omega_ordinal to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Apply In_irref (SNoLev x + SNoLev y) to the current goal.
We will
prove (SNoLev x + SNoLev y) ∈ (SNoLev x + SNoLev y).
We will
prove (SNoLev x + SNoLev y) ∈ SNoLev (x + y).
Apply H1 to the current goal.
We will
prove (SNoLev x + SNoLev y) ∈ ω.
An
exact proof term for the current goal is
add_SNo_In_omega (SNoLev x) Hx1 (SNoLev y) Hy1.
We will
prove SNo_ (SNoLev (x + y)) (x + y).
Apply SNoLev_ to the current goal.
An
exact proof term for the current goal is
SNo_add_SNo x y Hx3 Hy3.