Let x be given.
Assume Hx: SNo x.
Apply mul_SNo_eq_2 x 0 Hx SNo_0 to the current goal.
Let L and R be given.
Assume HLE HLI1 HLI2 HRE HRI1 HRI2 Hx0.
We will prove x * 0 = 0.
rewrite the current goal using Hx0 (from left to right).
We will prove SNoCut L R = 0.
We prove the intermediate claim LL0: L = 0.
Apply Empty_Subq_eq to the current goal.
Let w be given.
Assume Hw: w ∈ L.
We will prove False.
Apply HLE w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Let v be given.
rewrite the current goal using SNoL_0 (from left to right).
Assume Hv: v ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE v Hv.
Let u be given.
Assume Hu: u ∈ SNoR x.
Let v be given.
rewrite the current goal using SNoR_0 (from left to right).
Assume Hv: v ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE v Hv.
We prove the intermediate claim LR0: R = 0.
Apply Empty_Subq_eq to the current goal.
Let w be given.
Assume Hw: w ∈ R.
We will prove False.
Apply HRE w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoL x.
Let v be given.
rewrite the current goal using SNoR_0 (from left to right).
Assume Hv: v ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE v Hv.
Let u be given.
Assume Hu: u ∈ SNoR x.
Let v be given.
rewrite the current goal using SNoL_0 (from left to right).
Assume Hv: v ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE v Hv.
rewrite the current goal using LL0 (from left to right).
rewrite the current goal using LR0 (from left to right).
An exact proof term for the current goal is SNoCut_0_0.
∎