Let lambda be given.
Assume Hl1 Hl2.
Let L be given.
Assume HL.
Let R be given.
Assume HR HLR.
We prove the intermediate claim L1: ∀x ∈ L, SNoLev x ∈ lambda.
Let x be given.
Assume Hx.
Apply SNoS_E2 lambda Hl1 x (HL x Hx) to the current goal.
Assume H _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim L2: ∀y ∈ R, SNoLev y ∈ lambda.
Let y be given.
Assume Hy.
Apply SNoS_E2 lambda Hl1 y (HR y Hy) to the current goal.
Assume H _ _ _.
An exact proof term for the current goal is H.
We prove the intermediate claim L3: ordinal ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Apply ordinal_binunion to the current goal.
Apply ordinal_famunion to the current goal.
Let x be given.
Assume Hx.
Apply SNoS_E2 lambda Hl1 x (HL x Hx) to the current goal.
Assume _ H _ _.
We will prove ordinal (ordsucc (SNoLev x)).
Apply ordinal_ordsucc to the current goal.
We will prove ordinal (SNoLev x).
An exact proof term for the current goal is H.
Apply ordinal_famunion to the current goal.
Let y be given.
Assume Hy.
Apply SNoS_E2 lambda Hl1 y (HR y Hy) to the current goal.
Assume _ H _ _.
We will prove ordinal (ordsucc (SNoLev y)).
Apply ordinal_ordsucc to the current goal.
We will prove ordinal (SNoLev y).
An exact proof term for the current goal is H.
We prove the intermediate claim L4: ordinal (ordsucc lambda).
Apply ordinal_ordsucc to the current goal.
An exact proof term for the current goal is Hl1.
We prove the intermediate claim L5: ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))) ⊆ ordsucc lambda.
Apply ordinal_ordsucc_In_Subq to the current goal.
We will prove ordinal (ordsucc lambda).
An exact proof term for the current goal is L4.
We will prove ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))) ∈ ordsucc lambda.
Apply ordinal_In_Or_Subq ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))) (ordsucc lambda) L3 L4 to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1: ordsucc lambda ⊆ ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
We will prove False.
Apply binunionE (⋃x ∈ Lordsucc (SNoLev x)) (⋃y ∈ Rordsucc (SNoLev y)) lambda (H1 lambda (ordsuccI2 lambda)) to the current goal.
Assume H2: lambda ∈ ⋃x ∈ Lordsucc (SNoLev x).
Apply famunionE_impred L (λx ⇒ ordsucc (SNoLev x)) lambda H2 to the current goal.
Let x be given.
Assume Hx: x ∈ L.
Assume H3: lambda ∈ ordsucc (SNoLev x).
Apply In_no2cycle lambda (ordsucc (SNoLev x)) H3 to the current goal.
We will prove ordsucc (SNoLev x) ∈ lambda.
Apply Hl2 to the current goal.
An exact proof term for the current goal is L1 x Hx.
Assume H2: lambda ∈ ⋃y ∈ Rordsucc (SNoLev y).
Apply famunionE_impred R (λy ⇒ ordsucc (SNoLev y)) lambda H2 to the current goal.
Let y be given.
Assume Hy: y ∈ R.
Assume H3: lambda ∈ ordsucc (SNoLev y).
Apply In_no2cycle lambda (ordsucc (SNoLev y)) H3 to the current goal.
We will prove ordsucc (SNoLev y) ∈ lambda.
Apply Hl2 to the current goal.
An exact proof term for the current goal is L2 y Hy.
Apply SNoCutP_SNoCut_impred L R HLR 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 _ _ _.
An exact proof term for the current goal is L5 (SNoLev (SNoCut L R)) H2.
∎