Let α be given.
Assume Ha: ordinal α.
Let β be given.
Assume Hb: ordinal β.
Set Lo1 to be the term {x + β|x ∈ SNoS_ α}.
Set Lo2 to be the term {α + x|x ∈ SNoS_ β}.
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_ α) (λx ⇒ x + β) w H1 to the current goal.
Let x be given.
Assume Hx: x ∈ SNoS_ α.
Assume H2: w = x + β.
Apply SNoS_E2 α 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 + β).
An exact proof term for the current goal is SNo_add_SNo x β Hx2 (ordinal_SNo β Hb).
Assume H1: w ∈ Lo2.
Apply ReplE_impred (SNoS_ β) (λx ⇒ α + x) w H1 to the current goal.
Let x be given.
Assume Hx: x ∈ SNoS_ β.
Assume H2: w = α + x.
Apply SNoS_E2 β 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 (α + x).
An exact proof term for the current goal is SNo_add_SNo α x (ordinal_SNo α 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.
∎