Let v be given.
Let L and R be given.
Apply HLR to the current goal.
Assume HLR1.
Apply HLR1 to the current goal.
Set mL to be the term
{- w|w ∈ L}.
Set mR to be the term
{- z|z ∈ R}.
We prove the intermediate
claim L1:
SNo (SNoCut L R).
We prove the intermediate
claim L2:
SNoCutP mR mL.
We prove the intermediate
claim L3:
∀x ∈ mR, x < - v.
Let x be given.
Let z be given.
rewrite the current goal using Hxz (from left to right).
rewrite the current goal using HvLR (from left to right).
We prove the intermediate
claim L4:
∀y ∈ mL, - v < y.
Let y be given.
Let w be given.
rewrite the current goal using Hyw (from left to right).
rewrite the current goal using HvLR (from left to right).
An exact proof term for the current goal is H1.
An exact proof term for the current goal is Hv.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is Hv.
rewrite the current goal using
minus_SNo_Lev v Hv (from right to left).
An exact proof term for the current goal is H8.
An
exact proof term for the current goal is
IHv (SNoCut mR mL) L7 mR mL L2 (λq H ⇒ H).
We prove the intermediate
claim L8:
{- z|z ∈ mL} = L.
Let x be given.
An exact proof term for the current goal is Hx.
We prove the intermediate
claim L9:
{- z|z ∈ mR} = R.
Let y be given.
An exact proof term for the current goal is Hy.
We prove the intermediate
claim L10:
- SNoCut mR mL = v.
rewrite the current goal using LIH (from left to right).
rewrite the current goal using L8 (from left to right).
rewrite the current goal using L9 (from left to right).
Use symmetry.
An exact proof term for the current goal is HvLR.
rewrite the current goal using L10 (from right to left) at position 1.
rewrite the current goal using
minus_SNo_Lev v Hv (from right to left).
An exact proof term for the current goal is H8.
Use symmetry.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is H8.
An exact proof term for the current goal is H7.
∎