Let z be given.
Assume Hz: SNo z.
Set L to be the term SNoL z.
Set R to be the term SNoR z.
We prove the intermediate claim LLz: ordinal (SNoLev z).
An exact proof term for the current goal is SNoLev_ordinal z Hz.
We prove the intermediate claim L1: ∀x ∈ L, SNo x.
Let x be given.
Assume Hx: x ∈ L.
We will prove ∃α, ordinal α ∧ SNo_ α x.
We prove the intermediate claim L1a: x ∈ SNoS_ (SNoLev z).
An exact proof term for the current goal is SepE1 (SNoS_ (SNoLev z)) (λx ⇒ x < z) x Hx.
Apply SNoS_E (SNoLev z) LLz x L1a to the current goal.
Let β be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: β ∈ SNoLev z.
Assume H1: SNo_ β x.
We use β to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is ordinal_Hered (SNoLev z) LLz β Hb.
An exact proof term for the current goal is H1.
We prove the intermediate claim L2: ∀y ∈ R, SNo y.
Let y be given.
Assume Hy: y ∈ R.
We will prove ∃α, ordinal α ∧ SNo_ α y.
We prove the intermediate claim L2a: y ∈ SNoS_ (SNoLev z).
An exact proof term for the current goal is SepE1 (SNoS_ (SNoLev z)) (λy ⇒ z < y) y Hy.
Apply SNoS_E (SNoLev z) LLz y L2a to the current goal.
Let β be given.
Assume H1.
Apply H1 to the current goal.
Assume Hb: β ∈ SNoLev z.
Assume H1: SNo_ β y.
We use β to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is ordinal_Hered (SNoLev z) LLz β Hb.
An exact proof term for the current goal is H1.
We prove the intermediate claim L3: ∀x ∈ L, ∀y ∈ R, x < y.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Apply SNoLt_tra x z y (L1 x Hx) Hz (L2 y Hy) to the current goal.
We will prove x < z.
An exact proof term for the current goal is SepE2 (SNoS_ (SNoLev z)) (λx ⇒ x < z) x Hx.
We will prove z < y.
An exact proof term for the current goal is SepE2 (SNoS_ (SNoLev z)) (λy ⇒ z < y) y Hy.
We will prove SNoCutP L R.
We will prove (∀x ∈ L, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ L, ∀y ∈ R, x < y).
Apply and3I to the current goal.
An exact proof term for the current goal is L1.
An exact proof term for the current goal is L2.
An exact proof term for the current goal is L3.
∎