Apply SNoLev_ind2 to the current goal.
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume IHx: ∀w ∈ SNoS_ (SNoLev x), w + y = y + w.
Assume IHy: ∀z ∈ SNoS_ (SNoLev y), x + z = z + x.
Assume IHxy: ∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), w + z = z + w.
We prove the intermediate claim IHLx: ∀w ∈ SNoL x, w + y = y + w.
Let w be given.
Assume Hw: w ∈ SNoL x.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: w < x.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
An exact proof term for the current goal is IHx w Lw.
We prove the intermediate claim IHRx: ∀w ∈ SNoR x, w + y = y + w.
Let w be given.
Assume Hw: w ∈ SNoR x.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: x < w.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
An exact proof term for the current goal is IHx w Lw.
We prove the intermediate claim IHLy: ∀w ∈ SNoL y, x + w = w + x.
Let w be given.
Assume Hw: w ∈ SNoL y.
Apply SNoL_E y Hy w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: w < y.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 w y Hw1 Hy Hw2.
An exact proof term for the current goal is IHy w Lw.
We prove the intermediate claim IHRy: ∀w ∈ SNoR y, x + w = w + x.
Let w be given.
Assume Hw: w ∈ SNoR y.
Apply SNoR_E y Hy w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev y.
Assume Hw3: y < w.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 w y Hw1 Hy Hw2.
An exact proof term for the current goal is IHy w Lw.
We will prove x + y = y + x.
Set Lxy1 to be the term {w + y|w ∈ SNoL x}.
Set Lxy2 to be the term {x + w|w ∈ SNoL y}.
Set Rxy1 to be the term {z + y|z ∈ SNoR x}.
Set Rxy2 to be the term {x + z|z ∈ SNoR y}.
rewrite the current goal using add_SNo_eq x Hx y Hy (from left to right).
We will prove (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) = y + x.
Set Lyx1 to be the term {w + x|w ∈ SNoL y}.
Set Lyx2 to be the term {y + w|w ∈ SNoL x}.
Set Ryx1 to be the term {z + x|z ∈ SNoR y}.
Set Ryx2 to be the term {y + z|z ∈ SNoR x}.
rewrite the current goal using add_SNo_eq y Hy x Hx (from left to right).
We will prove (SNoCut (Lxy1 ∪ Lxy2) (Rxy1 ∪ Rxy2)) = (SNoCut (Lyx1 ∪ Lyx2) (Ryx1 ∪ Ryx2)).
We prove the intermediate claim Lxy1yx2: Lxy1 = Lyx2.
We will prove {w + y|w ∈ SNoL x} = {y + w|w ∈ SNoL x}.
Apply ReplEq_ext (SNoL x) (λw ⇒ w + y) (λw ⇒ y + w) to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
We will prove w + y = y + w.
An exact proof term for the current goal is IHLx w Hw.
We prove the intermediate claim Lxy2yx1: Lxy2 = Lyx1.
We will prove {x + w|w ∈ SNoL y} = {w + x|w ∈ SNoL y}.
Apply ReplEq_ext (SNoL y) (λw ⇒ x + w) (λw ⇒ w + x) to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL y.
We will prove x + w = w + x.
An exact proof term for the current goal is IHLy w Hw.
We prove the intermediate claim Rxy1yx2: Rxy1 = Ryx2.
We will prove {w + y|w ∈ SNoR x} = {y + w|w ∈ SNoR x}.
Apply ReplEq_ext (SNoR x) (λw ⇒ w + y) (λw ⇒ y + w) to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
We will prove w + y = y + w.
An exact proof term for the current goal is IHRx w Hw.
We prove the intermediate claim Rxy2yx1: Rxy2 = Ryx1.
We will prove {x + w|w ∈ SNoR y} = {w + x|w ∈ SNoR y}.
Apply ReplEq_ext (SNoR y) (λw ⇒ x + w) (λw ⇒ w + x) to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR y.
We will prove x + w = w + x.
An exact proof term for the current goal is IHRy w Hw.
rewrite the current goal using Lxy1yx2 (from left to right).
rewrite the current goal using Lxy2yx1 (from left to right).
rewrite the current goal using Rxy1yx2 (from left to right).
rewrite the current goal using Rxy2yx1 (from left to right).
We will prove (SNoCut (Lyx2 ∪ Lyx1) (Ryx2 ∪ Ryx1)) = (SNoCut (Lyx1 ∪ Lyx2) (Ryx1 ∪ Ryx2)).
rewrite the current goal using binunion_com Lyx2 Lyx1 (from left to right).
rewrite the current goal using binunion_com Ryx2 Ryx1 (from left to right).
Use reflexivity.
∎