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.
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.
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.
An exact proof term for the current goal is Hl1.
An exact proof term for the current goal is L4.
Assume H1.
An exact proof term for the current goal is H1.
Let x be given.
Apply Hl2 to the current goal.
An exact proof term for the current goal is L1 x Hx.
Let y be given.
Apply Hl2 to the current goal.
An exact proof term for the current goal is L2 y Hy.
Assume _ _ _.
An
exact proof term for the current goal is
L5 (SNoLev (SNoCut L R)) H2.
∎