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 LC: SNoCutP L R.
An exact proof term for the current goal is SNoCutP_SNoL_SNoR z Hz.
Apply SNoCutP_SNoCut L R LC to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: SNo (SNoCut L R).
Assume H2: SNoLev (SNoCut L R) ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume H3: ∀x ∈ L, x < SNoCut L R.
Assume H4: ∀y ∈ R, SNoCut L R < y.
Assume H5: ∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ PNoEq_ (SNoLev (SNoCut L R)) (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z).
We prove the intermediate claim L4: ordinal (SNoLev (SNoCut L R)).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is H1.
We prove the intermediate claim L5: ∀x ∈ L, x < z.
Let x be given.
Assume Hx: x ∈ L.
An exact proof term for the current goal is SepE2 (SNoS_ (SNoLev z)) (λx ⇒ x < z) x Hx.
We prove the intermediate claim L6: ∀y ∈ R, z < y.
Let y be given.
Assume Hy: y ∈ R.
An exact proof term for the current goal is SepE2 (SNoS_ (SNoLev z)) (λy ⇒ z < y) y Hy.
Apply H5 z Hz L5 L6 to the current goal.
Assume H6: SNoLev (SNoCut L R) ⊆ SNoLev z.
Assume H7: PNoEq_ (SNoLev (SNoCut L R)) (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z).
We prove the intermediate claim L7: SNoLev (SNoCut L R) = SNoLev z.
Apply ordinal_trichotomy_or (SNoLev (SNoCut L R)) (SNoLev z) L4 LLz to the current goal.
Assume H8.
Apply H8 to the current goal.
Assume H8: SNoLev (SNoCut L R) ∈ SNoLev z.
We will prove False.
Apply SNoLt_trichotomy_or z (SNoCut L R) Hz H1 to the current goal.
Assume H9.
Apply H9 to the current goal.
Assume H9: z < SNoCut L R.
Apply SNoLt_irref (SNoCut L R) to the current goal.
Apply H4 to the current goal.
We will prove SNoCut L R ∈ R.
We will prove SNoCut L R ∈ {y ∈ SNoS_ (SNoLev z)|z < y}.
Apply SepI to the current goal.
Apply SNoS_I (SNoLev z) LLz (SNoCut L R) (SNoLev (SNoCut L R)) H8 to the current goal.
We will prove SNo_ (SNoLev (SNoCut L R)) (SNoCut L R).
An exact proof term for the current goal is SNoLev_ (SNoCut L R) H1.
We will prove z < SNoCut L R.
An exact proof term for the current goal is H9.
Assume H9: z = SNoCut L R.
Apply In_irref (SNoLev z) to the current goal.
rewrite the current goal using H9 (from left to right) at position 1.
An exact proof term for the current goal is H8.
Assume H9: SNoCut L R < z.
Apply SNoLt_irref (SNoCut L R) to the current goal.
Apply H3 to the current goal.
We will prove SNoCut L R ∈ L.
We will prove SNoCut L R ∈ {x ∈ SNoS_ (SNoLev z)|x < z}.
Apply SepI to the current goal.
Apply SNoS_I (SNoLev z) LLz (SNoCut L R) (SNoLev (SNoCut L R)) H8 to the current goal.
We will prove SNo_ (SNoLev (SNoCut L R)) (SNoCut L R).
An exact proof term for the current goal is SNoLev_ (SNoCut L R) H1.
We will prove SNoCut L R < z.
An exact proof term for the current goal is H9.
Assume H8: SNoLev (SNoCut L R) = SNoLev z.
An exact proof term for the current goal is H8.
Assume H8: SNoLev z ∈ SNoLev (SNoCut L R).
We will prove False.
Apply In_irref (SNoLev z) to the current goal.
Apply H6 to the current goal.
An exact proof term for the current goal is H8.
We will prove z = SNoCut L R.
Use symmetry.
We will prove SNoCut L R = z.
Apply SNo_eq to the current goal.
We will prove SNo (SNoCut L R).
An exact proof term for the current goal is H1.
We will prove SNo z.
An exact proof term for the current goal is Hz.
We will prove SNoLev (SNoCut L R) = SNoLev z.
An exact proof term for the current goal is L7.
We will prove ∀alpha ∈ SNoLev (SNoCut L R), alpha ∈ SNoCut L R ↔ alpha ∈ z.
An exact proof term for the current goal is H7.
∎