Let z be given.
Assume Hz: SNo z.
Let p be given.
Assume H1.
We prove the intermediate claim LLz: ordinal (SNoLev z).
An exact proof term for the current goal is SNoLev_ordinal z Hz.
Set L to be the term {x ∈ SNoS_ (SNoLev z)|x < z}.
Set R to be the term {y ∈ SNoS_ (SNoLev z)|z < y}.
We prove the intermediate claim L1: z = SNoCut L R.
An exact proof term for the current goal is SNo_eta z Hz.
We prove the intermediate claim LL: ∀x, x ∈ L → SNo x ∧ SNoLev x ∈ SNoLev z ∧ x < z.
Let x be given.
Assume Hx: x ∈ L.
Apply SepE (SNoS_ (SNoLev z)) (λx ⇒ x < z) x Hx to the current goal.
Assume Hx1: x ∈ SNoS_ (SNoLev z).
Assume Hx2: x < z.
Apply SNoS_E (SNoLev z) LLz x Hx1 to the current goal.
Let β be given.
Assume Hx3.
Apply Hx3 to the current goal.
Assume Hb: β ∈ SNoLev z.
Assume Hx3: SNo_ β x.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered (SNoLev z) LLz β Hb.
We prove the intermediate claim Lx1: SNo x.
We will prove ∃α, ordinal α ∧ SNo_ α x.
We use β to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lb.
An exact proof term for the current goal is Hx3.
We prove the intermediate claim Lx2: SNoLev x = β.
Apply SNoLev_prop x Lx1 to the current goal.
Assume Hx4: ordinal (SNoLev x).
Assume Hx5: SNo_ (SNoLev x) x.
Apply SNoLev_uniq x to the current goal.
An exact proof term for the current goal is Hx4.
An exact proof term for the current goal is Lb.
Apply Hx5 to the current goal.
An exact proof term for the current goal is Hx3.
We prove the intermediate claim Lx3: SNoLev x ∈ SNoLev z.
rewrite the current goal using Lx2 (from left to right).
An exact proof term for the current goal is Hb.
Apply and3I to the current goal.
We will prove SNo x.
An exact proof term for the current goal is Lx1.
We will prove SNoLev x ∈ SNoLev z.
An exact proof term for the current goal is Lx3.
We will prove x < z.
An exact proof term for the current goal is Hx2.
We prove the intermediate claim LR: ∀y, y ∈ R → SNo y ∧ SNoLev y ∈ SNoLev z ∧ z < y.
Let y be given.
Assume Hy: y ∈ R.
Apply SepE (SNoS_ (SNoLev z)) (λy ⇒ z < y) y Hy to the current goal.
Assume Hy1: y ∈ SNoS_ (SNoLev z).
Assume Hy2: z < y.
Apply SNoS_E (SNoLev z) LLz y Hy1 to the current goal.
Let β be given.
Assume Hy3.
Apply Hy3 to the current goal.
Assume Hb: β ∈ SNoLev z.
Assume Hy3: SNo_ β y.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered (SNoLev z) LLz β Hb.
We prove the intermediate claim Ly1: SNo y.
We will prove ∃α, ordinal α ∧ SNo_ α y.
We use β to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lb.
An exact proof term for the current goal is Hy3.
We prove the intermediate claim Ly2: SNoLev y = β.
Apply SNoLev_prop y Ly1 to the current goal.
Assume Hy4: ordinal (SNoLev y).
Assume Hy5: SNo_ (SNoLev y) y.
Apply SNoLev_uniq y to the current goal.
An exact proof term for the current goal is Hy4.
An exact proof term for the current goal is Lb.
Apply Hy5 to the current goal.
An exact proof term for the current goal is Hy3.
We prove the intermediate claim Ly3: SNoLev y ∈ SNoLev z.
rewrite the current goal using Ly2 (from left to right).
An exact proof term for the current goal is Hb.
Apply and3I to the current goal.
We will prove SNo y.
An exact proof term for the current goal is Ly1.
We will prove SNoLev y ∈ SNoLev z.
An exact proof term for the current goal is Ly3.
We will prove z < y.
An exact proof term for the current goal is Hy2.
Apply H1 L R to the current goal.
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.
Let x be given.
Assume Hx.
Apply LL x Hx to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
An exact proof term for the current goal is H.
Let y be given.
Assume Hy.
Apply LR y Hy to the current goal.
Assume H _.
Apply H to the current goal.
Assume H _.
An exact proof term for the current goal is H.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
Apply LL x Hx to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: SNo x.
Assume H3: SNoLev x ∈ SNoLev z.
Assume H4: x < z.
Apply LR y Hy to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: SNo y.
Assume H6: SNoLev y ∈ SNoLev z.
Assume H7: z < y.
An exact proof term for the current goal is SNoLt_tra x z y H2 Hz H5 H4 H7.
We will prove ∀x ∈ L, SNoLev x ∈ SNoLev z.
Let x be given.
Assume Hx.
Apply LL x Hx to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We will prove ∀y ∈ R, SNoLev y ∈ SNoLev z.
Let y be given.
Assume Hy.
Apply LR y Hy to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We will prove z = SNoCut L R.
An exact proof term for the current goal is L1.
∎