Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume Hx1: SNoLev x ∈ ω.
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 Hy1: SNoLev y ∈ ω.
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.
Assume H1: ω ⊆ SNoLev (x + y).
Apply In_irref (SNoLev x + SNoLev y) to the current goal.
We will prove (SNoLev x + SNoLev y) ∈ (SNoLev x + SNoLev y).
Apply add_SNo_Lev_bd x y Hx3 Hy3 to the current goal.
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.
∎