Let L and R be given.
Apply HLR to the current goal.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim LCLR:
SNo (SNoCut L R).
We prove the intermediate
claim LmCLR:
SNo (- SNoCut L R).
An exact proof term for the current goal is LCLR.
We prove the intermediate
claim LmmCLR:
SNo (- - SNoCut L R).
An exact proof term for the current goal is LmCLR.
An exact proof term for the current goal is HLR.
An exact proof term for the current goal is LmmCLR.
Let x be given.
Assume Hx.
rewrite the current goal using IHL x Hx (from right to left).
We prove the intermediate
claim Lx:
SNo x.
An exact proof term for the current goal is HLR1 x Hx.
We prove the intermediate
claim Lmx:
SNo (- x).
Let y be given.
Assume Hy.
rewrite the current goal using IHR y Hy (from right to left).
We prove the intermediate
claim Ly:
SNo y.
An exact proof term for the current goal is HLR2 y Hy.
We prove the intermediate
claim Lmy:
SNo (- y).
Apply L1 to the current goal.
Use symmetry.
Apply SNo_eq to the current goal.
An exact proof term for the current goal is LCLR.
An exact proof term for the current goal is LmmCLR.
An exact proof term for the current goal is L1a.
An exact proof term for the current goal is L1b.
∎