Let z be given.
Set L to be the term
SNoL z.
Set R to be the term
SNoR z.
We prove the intermediate
claim LC:
SNoCutP L R.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
An exact proof term for the current goal is H1.
We prove the intermediate
claim L5:
∀x ∈ L, x < z.
Let x be given.
An
exact proof term for the current goal is
SepE2 (SNoS_ (SNoLev z)) (λx ⇒ x < z) x Hx.
We prove the intermediate
claim L6:
∀y ∈ R, z < y.
Let y be given.
An
exact proof term for the current goal is
SepE2 (SNoS_ (SNoLev z)) (λy ⇒ z < y) y Hy.
Apply H5 z Hz L5 L6 to the current goal.
Assume H8.
Apply H8 to the current goal.
Assume H9.
Apply H9 to the current goal.
Apply H4 to the current goal.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoLev_ (SNoCut L R) H1.
An exact proof term for the current goal is H9.
rewrite the current goal using H9 (from left to right) at position 1.
An exact proof term for the current goal is H8.
Apply H3 to the current goal.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoLev_ (SNoCut L R) H1.
An exact proof term for the current goal is H9.
An exact proof term for the current goal is H8.
Apply H6 to the current goal.
An exact proof term for the current goal is H8.
Use symmetry.
Apply SNo_eq to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is Hz.
An exact proof term for the current goal is L7.
An exact proof term for the current goal is H7.
∎