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.
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.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate
claim L1:
SNoCutP L R.
Apply and3I to the current goal.
Let w be given.
Let n be given.
Assume Hn.
rewrite the current goal using Hwn (from left to right).
An exact proof term for the current goal is Lf n Hn.
Let z be given.
Let m be given.
Assume Hm.
rewrite the current goal using Hzm (from left to right).
An exact proof term for the current goal is Lg m Hm.
Let w be given.
Let z be given.
Let n be given.
Assume Hn.
rewrite the current goal using Hwn (from left to right).
Let m be given.
Assume Hm.
rewrite the current goal using Hzm (from left to right).
An exact proof term for the current goal is Hfg n Hn m Hm.
We prove the intermediate
claim L2:
L ⊆ SNoS_ ω.
Let w be given.
Assume Hw.
Let n be given.
Assume Hn.
rewrite the current goal using Hwn (from left to right).
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.
Let m be given.
Assume Hm.
rewrite the current goal using Hzm (from left to right).
An
exact proof term for the current goal is
(ap_Pi ω (λ_ ⇒ SNoS_ ω) g m Hg1 Hm).
An exact proof term for the current goal is L4.
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.
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.
Apply HLR4 to the current goal.
An
exact proof term for the current goal is
ReplI ω (λn ⇒ g n) n Hn.
∎