Let L and R be given.
Assume HLR.
Set y to be the term SNoCut L R.
Let z be given.
Assume Hz: z ∈ SNoR y.
Apply dneg to the current goal.
Assume HC: ¬ ∃z' ∈ R, z' ≤ z.
Apply HLR to the current goal.
Assume H.
Apply H to the current goal.
Assume HL HR HLR'.
Apply SNoCutP_SNoCut_impred L R HLR to the current goal.
Assume H1: SNo y.
Assume H2: SNoLev y ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume H3: ∀w ∈ L, w < y.
Assume H4: ∀z ∈ R, y < z.
Assume H5: ∀u, SNo u → (∀w ∈ L, w < u) → (∀z ∈ R, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u.
Apply SNoR_E y H1 z Hz to the current goal.
Assume Hz1 Hz2 Hz3.
We prove the intermediate claim L1: SNoLev y ⊆ SNoLev z ∧ SNoEq_ (SNoLev y) y z.
Apply H5 z Hz1 to the current goal.
Let w be given.
Assume Hw: w ∈ L.
We will prove w < z.
Apply SNoLt_tra w y z (HL w Hw) H1 Hz1 to the current goal.
We will prove w < y.
An exact proof term for the current goal is H3 w Hw.
We will prove y < z.
An exact proof term for the current goal is Hz3.
Let z' be given.
Assume Hz': z' ∈ R.
We will prove z < z'.
Apply SNoLtLe_or z z' Hz1 (HR z' Hz') to the current goal.
Assume H6.
An exact proof term for the current goal is H6.
Assume H6: z' ≤ z.
Apply HC to the current goal.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
An exact proof term for the current goal is H6.
Apply In_irref (SNoLev z) to the current goal.
We will prove SNoLev z ∈ SNoLev z.
Apply andEL (SNoLev y ⊆ SNoLev z) (SNoEq_ (SNoLev y) y z) L1 to the current goal.
We will prove SNoLev z ∈ SNoLev y.
An exact proof term for the current goal is Hz2.
∎