Let L and R be given.

Assume HLR.

Set y to be the term SNoCut L R.

Let w be given.

Assume Hw: w ∈ SNoL y.

Apply dneg to the current goal.

Assume HC: ¬ ∃w' ∈ L, w ≤ w'.

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 ∈ L}ordsucc (SNoLev x)) ∪ (⋃_{y ∈ R}ordsucc (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 SNoL_E y H1 w Hw to the current goal.

Assume Hw1 Hw2 Hw3.

We prove the intermediate claim L1: SNoLev y ⊆ SNoLev w ∧ SNoEq_ (SNoLev y) y w.

Apply H5 w Hw1 to the current goal.

Let w' be given.

Assume Hw': w' ∈ L.

We will prove w' < w.

Apply SNoLtLe_or w' w (HL w' Hw') Hw1 to the current goal.

Assume H6.

An exact proof term for the current goal is H6.

Assume H6: w ≤ w'.

Apply HC to the current goal.

We use w' to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hw'.

An exact proof term for the current goal is H6.

Let z be given.

Assume Hz: z ∈ R.

We will prove w < z.

Apply SNoLt_tra w y z Hw1 H1 (HR z Hz) Hw3 to the current goal.

We will prove y < z.

An exact proof term for the current goal is H4 z Hz.

Apply In_irref (SNoLev w) to the current goal.

We will prove SNoLev w ∈ SNoLev w.

Apply andEL (SNoLev y ⊆ SNoLev w) (SNoEq_ (SNoLev y) y w) L1 to the current goal.

We will prove SNoLev w ∈ SNoLev y.

An exact proof term for the current goal is Hw2.

∎