Let L1, R1, L2 and R2 be given.
Assume HLR1 HLR2.
Assume H1: ∀w ∈ L1, w < SNoCut L2 R2.
Assume H2: ∀z ∈ R2, SNoCut L1 R1 < z.
Apply HLR1 to the current goal.
Assume HLR1a.
Apply HLR1a to the current goal.
Assume HLR1a: ∀x ∈ L1, SNo x.
Assume HLR1b: ∀y ∈ R1, SNo y.
Assume HLR1c: ∀x ∈ L1, ∀y ∈ R1, x < y.
Apply HLR2 to the current goal.
Assume HLR2a.
Apply HLR2a to the current goal.
Assume HLR2a: ∀x ∈ L2, SNo x.
Assume HLR2b: ∀y ∈ R2, SNo y.
Assume HLR2c: ∀x ∈ L2, ∀y ∈ R2, x < y.
Set alpha to be the term ⋃x ∈ L1ordsucc (SNoLev x).
Set beta to be the term ⋃y ∈ R1ordsucc (SNoLev y).
Set gamma to be the term ⋃x ∈ L2ordsucc (SNoLev x).
Set delta to be the term ⋃y ∈ R2ordsucc (SNoLev y).
Apply SNoCutP_SNoCut L1 R1 HLR1 to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume H3: SNo (SNoCut L1 R1).
Assume H4: SNoLev (SNoCut L1 R1) ∈ ordsucc (α ∪ β).
Assume H5: ∀x ∈ L1, x < SNoCut L1 R1.
Assume H6: ∀y ∈ R1, SNoCut L1 R1 < y.
Assume H7: ∀z, SNo z → (∀x ∈ L1, x < z) → (∀y ∈ R1, z < y) → SNoLev (SNoCut L1 R1) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L1 R1)) (SNoCut L1 R1) z.
Apply SNoCutP_SNoCut L2 R2 HLR2 to the current goal.
Assume H8.
Apply H8 to the current goal.
Assume H8.
Apply H8 to the current goal.
Assume H8.
Apply H8 to the current goal.
Assume H8: SNo (SNoCut L2 R2).
Assume H9: SNoLev (SNoCut L2 R2) ∈ ordsucc (γ ∪ δ).
Assume H10: ∀x ∈ L2, x < SNoCut L2 R2.
Assume H11: ∀y ∈ R2, SNoCut L2 R2 < y.
Assume H12: ∀z, SNo z → (∀x ∈ L2, x < z) → (∀y ∈ R2, z < y) → SNoLev (SNoCut L2 R2) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L2 R2)) (SNoCut L2 R2) z.
Apply SNoLtLe_or (SNoCut L2 R2) (SNoCut L1 R1) H8 H3 to the current goal.
Assume H13: SNoCut L2 R2 < SNoCut L1 R1.
We will prove False.
Apply SNoLtE (SNoCut L2 R2) (SNoCut L1 R1) H8 H3 H13 to the current goal.
Let z be given.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev (SNoCut L2 R2) ∩ SNoLev (SNoCut L1 R1).
Assume Hz3: SNoEq_ (SNoLev z) z (SNoCut L2 R2).
Assume Hz4: SNoEq_ (SNoLev z) z (SNoCut L1 R1).
Assume Hz5: (SNoCut L2 R2) < z.
Assume Hz6: z < (SNoCut L1 R1).
Assume Hz7: SNoLev z ∉ (SNoCut L2 R2).
Assume Hz8: SNoLev z ∈ (SNoCut L1 R1).
We prove the intermediate claim LzL1: ∀x ∈ L1, x < z.
Let x be given.
Assume Hx: x ∈ L1.
Apply SNoLt_tra x (SNoCut L2 R2) z (HLR1a x Hx) H8 Hz1 to the current goal.
We will prove x < SNoCut L2 R2.
An exact proof term for the current goal is H1 x Hx.
We will prove SNoCut L2 R2 < z.
An exact proof term for the current goal is Hz5.
We prove the intermediate claim LzR1: ∀y ∈ R1, z < y.
Let y be given.
Assume Hy: y ∈ R1.
Apply SNoLt_tra z (SNoCut L1 R1) y Hz1 H3 (HLR1b y Hy) to the current goal.
We will prove z < SNoCut L1 R1.
An exact proof term for the current goal is Hz6.
We will prove SNoCut L1 R1 < y.
An exact proof term for the current goal is H6 y Hy.
Apply H7 z Hz1 LzL1 LzR1 to the current goal.
Assume H14: SNoLev (SNoCut L1 R1) ⊆ SNoLev z.
Assume _.
Apply In_irref (SNoLev z) to the current goal.
Apply H14 to the current goal.
We will prove SNoLev z ∈ SNoLev (SNoCut L1 R1).
An exact proof term for the current goal is binintersectE2 (SNoLev (SNoCut L2 R2)) (SNoLev (SNoCut L1 R1)) (SNoLev z) Hz2.
Assume H14: SNoLev (SNoCut L2 R2) ∈ SNoLev (SNoCut L1 R1).
Assume H15: SNoEq_ (SNoLev (SNoCut L2 R2)) (SNoCut L2 R2) (SNoCut L1 R1).
Assume H16: SNoLev (SNoCut L2 R2) ∈ (SNoCut L1 R1).
Set z to be the term SNoCut L2 R2.
We prove the intermediate claim LzR1: ∀y ∈ R1, z < y.
Let y be given.
Assume Hy: y ∈ R1.
Apply SNoLt_tra z (SNoCut L1 R1) y H8 H3 (HLR1b y Hy) to the current goal.
We will prove z < SNoCut L1 R1.
An exact proof term for the current goal is H13.
We will prove SNoCut L1 R1 < y.
An exact proof term for the current goal is H6 y Hy.
Apply H7 z H8 H1 LzR1 to the current goal.
Assume H17: SNoLev (SNoCut L1 R1) ⊆ SNoLev z.
Assume _.
Apply In_irref (SNoLev z) to the current goal.
Apply H17 to the current goal.
We will prove SNoLev z ∈ SNoLev (SNoCut L1 R1).
An exact proof term for the current goal is H14.
Assume H14: SNoLev (SNoCut L1 R1) ∈ SNoLev (SNoCut L2 R2).
Assume H15: SNoEq_ (SNoLev (SNoCut L1 R1)) (SNoCut L2 R2) (SNoCut L1 R1).
Assume H16: SNoLev (SNoCut L1 R1) ∉ (SNoCut L2 R2).
Set z to be the term SNoCut L1 R1.
We prove the intermediate claim LzL2: ∀x ∈ L2, x < z.
Let x be given.
Assume Hx: x ∈ L2.
Apply SNoLt_tra x (SNoCut L2 R2) z (HLR2a x Hx) H8 H3 to the current goal.
We will prove x < SNoCut L2 R2.
An exact proof term for the current goal is H10 x Hx.
We will prove SNoCut L2 R2 < z.
An exact proof term for the current goal is H13.
Apply H12 z H3 LzL2 H2 to the current goal.
Assume H17: SNoLev (SNoCut L2 R2) ⊆ SNoLev z.
Assume _.
Apply In_irref (SNoLev z) to the current goal.
Apply H17 to the current goal.
We will prove SNoLev z ∈ SNoLev (SNoCut L2 R2).
An exact proof term for the current goal is H14.
Assume H13: SNoCut L1 R1 ≤ SNoCut L2 R2.
An exact proof term for the current goal is H13.
∎