Let f be given.
Assume Hf1.
Let g be given.
Assume Hg1 Hfg.
Let p be given.
Assume Hp.
Set L to be the term {f n|n ∈ ω}.
Set R to be the term {g n|n ∈ ω}.
Set x to be the term SNoCut L R.
We prove the intermediate claim Lf: ∀n ∈ ω, SNo (f n).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (f n) (ap_Pi ω (λ_ ⇒ SNoS_ ω) f n Hf1 Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lg: ∀n ∈ ω, SNo (g n).
Let n be given.
Assume Hn.
Apply SNoS_E2 ω omega_ordinal (g n) (ap_Pi ω (λ_ ⇒ SNoS_ ω) g n Hg1 Hn) to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim L1: SNoCutP L R.
We will prove (∀w ∈ L, SNo w) ∧ (∀z ∈ R, SNo z) ∧ (∀w ∈ L, ∀z ∈ R, w < z).
Apply and3I to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Apply ReplE_impred ω (λn ⇒ f n) w Hw to the current goal.
Let n be given.
Assume Hn.
Assume Hwn: w = f n.
rewrite the current goal using Hwn (from left to right).
We will prove SNo (f n).
An exact proof term for the current goal is Lf n Hn.
Let z be given.
Assume Hz: z ∈ R.
Apply ReplE_impred ω (λn ⇒ g n) z Hz to the current goal.
Let m be given.
Assume Hm.
Assume Hzm: z = g m.
rewrite the current goal using Hzm (from left to right).
We will prove SNo (g m).
An exact proof term for the current goal is Lg m Hm.
Let w be given.
Assume Hw: w ∈ L.
Let z be given.
Assume Hz: z ∈ R.
Apply ReplE_impred ω (λn ⇒ f n) w Hw to the current goal.
Let n be given.
Assume Hn.
Assume Hwn: w = f n.
rewrite the current goal using Hwn (from left to right).
Apply ReplE_impred ω (λn ⇒ g n) z Hz to the current goal.
Let m be given.
Assume Hm.
Assume Hzm: z = g m.
rewrite the current goal using Hzm (from left to right).
We will prove f n < g m.
An exact proof term for the current goal is Hfg n Hn m Hm.
Apply SNoCutP_SNoCut_impred L R L1 to the current goal.
Assume HLR1: SNo x.
Assume HLR2: SNoLev x ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume HLR3: ∀w ∈ L, w < x.
Assume HLR4: ∀y ∈ R, x < y.
Assume HLR5: ∀z, SNo z → (∀w ∈ L, w < z) → (∀y ∈ R, z < y) → SNoLev x ⊆ SNoLev z ∧ SNoEq_ (SNoLev x) x z.
We prove the intermediate claim L2: L ⊆ SNoS_ ω.
Let w be given.
Assume Hw.
Apply ReplE_impred ω (λn ⇒ f n) w Hw to the current goal.
Let n be given.
Assume Hn.
Assume Hwn: w = f n.
rewrite the current goal using Hwn (from left to right).
We will prove f n ∈ SNoS_ ω.
An exact proof term for the current goal is ap_Pi ω (λ_ ⇒ SNoS_ ω) f n Hf1 Hn.
We prove the intermediate claim L3: R ⊆ SNoS_ ω.
Let z be given.
Assume Hz: z ∈ R.
Apply ReplE_impred ω (λn ⇒ g n) z Hz to the current goal.
Let m be given.
Assume Hm.
Assume Hzm: z = g m.
rewrite the current goal using Hzm (from left to right).
We will prove g m ∈ SNoS_ ω.
An exact proof term for the current goal is (ap_Pi ω (λ_ ⇒ SNoS_ ω) g m Hg1 Hm).
We prove the intermediate claim L4: SNoLev x ∈ ordsucc ω.
An exact proof term for the current goal is SNoCutP_SNoCut_omega L L2 R L3 L1.
We prove the intermediate claim L5: x ∈ SNoS_ (ordsucc ω).
Apply SNoS_I (ordsucc ω) ordsucc_omega_ordinal x (SNoLev x) to the current goal.
We will prove SNoLev x ∈ ordsucc ω.
An exact proof term for the current goal is L4.
We will prove SNo_ (SNoLev x) x.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is HLR1.
Apply Hp L1 HLR1 L4 L5 to the current goal.
Let n be given.
Assume Hn.
We will prove f n < x.
Apply HLR3 to the current goal.
An exact proof term for the current goal is ReplI ω (λn ⇒ f n) n Hn.
Let n be given.
Assume Hn.
We will prove x < g n.
Apply HLR4 to the current goal.
An exact proof term for the current goal is ReplI ω (λn ⇒ g n) n Hn.
∎