Let alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: ordinal beta.
Set Lo1 to be the term {x + beta|x ∈ SNoS_ alpha}.
Set Lo2 to be the term {alpha + x|x ∈ SNoS_ beta}.
We will prove (∀x ∈ Lo1 ∪ Lo2, SNo x) ∧ (∀y ∈ Empty, SNo y) ∧ (∀x ∈ Lo1 ∪ Lo2, ∀y ∈ Empty, x < y).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ Lo1 ∪ Lo2.
Apply binunionE Lo1 Lo2 w Hw to the current goal.
Assume H1: w ∈ Lo1.
Apply ReplE_impred (SNoS_ alpha) (λx ⇒ x + beta) w H1 to the current goal.
Let x be given.
Assume Hx: x ∈ SNoS_ alpha.
Assume H2: w = x + beta.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Assume _ _.
Assume Hx2: SNo x.
Assume _.
We will prove SNo w.
rewrite the current goal using H2 (from left to right).
We will prove SNo (x + beta).
An exact proof term for the current goal is SNo_add_SNo x beta Hx2 (ordinal_SNo beta Hb).
Assume H1: w ∈ Lo2.
Apply ReplE_impred (SNoS_ beta) (λx ⇒ alpha + x) w H1 to the current goal.
Let x be given.
Assume Hx: x ∈ SNoS_ beta.
Assume H2: w = alpha + x.
Apply SNoS_E2 beta Hb x Hx to the current goal.
Assume _ _.
Assume Hx2: SNo x.
Assume _.
We will prove SNo w.
rewrite the current goal using H2 (from left to right).
We will prove SNo (alpha + x).
An exact proof term for the current goal is SNo_add_SNo alpha x (ordinal_SNo alpha Ha) Hx2.
Let y be given.
Assume Hy: y ∈ Empty.
We will prove False.
An exact proof term for the current goal is EmptyE y Hy.
Let x be given.
Assume _.
Let y be given.
Assume Hy: y ∈ Empty.
We will prove False.
An exact proof term for the current goal is EmptyE y Hy.
∎