Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), 0 + w = w.
We will prove 0 + x = x.
rewrite the current goal using add_SNo_eq 0 SNo_0 x Hx (from left to right).
We will prove SNoCut ({w + x|w ∈ SNoL 0} ∪ {0 + w|w ∈ SNoL x}) ({w + x|w ∈ SNoR 0} ∪ {0 + w|w ∈ SNoR x}) = x.
We prove the intermediate claim L1: {w + x|w ∈ SNoL 0} ∪ {0 + w|w ∈ SNoL x} = SNoL x.
rewrite the current goal using SNoL_0 (from left to right).
We will prove {w + x|w ∈ Empty} ∪ {0 + w|w ∈ SNoL x} = SNoL x.
rewrite the current goal using Repl_Empty (λw ⇒ w + x) (from left to right).
We will prove Empty ∪ {0 + w|w ∈ SNoL x} = SNoL x.
rewrite the current goal using binunion_idl (from left to right).
We will prove {0 + w|w ∈ SNoL x} = SNoL x.
Apply set_ext to the current goal.
Let u be given.
Assume Hu: u ∈ {0 + w|w ∈ SNoL x}.
Apply ReplE_impred (SNoL x) (λw ⇒ 0 + w) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
Assume H1: u = 0 + w.
We will prove u ∈ SNoL x.
rewrite the current goal using H1 (from left to right).
We will prove 0 + w ∈ SNoL x.
rewrite the current goal using IH w (SNoL_SNoS_ x w Hw) (from left to right).
We will prove w ∈ SNoL x.
An exact proof term for the current goal is Hw.
Let u be given.
Assume Hu: u ∈ SNoL x.
We will prove u ∈ {0 + w|w ∈ SNoL x}.
rewrite the current goal using IH u (SNoL_SNoS_ x u Hu) (from right to left).
We will prove 0 + u ∈ {0 + w|w ∈ SNoL x}.
An exact proof term for the current goal is ReplI (SNoL x) (λw ⇒ 0 + w) u Hu.
We prove the intermediate claim L2: {w + x|w ∈ SNoR 0} ∪ {0 + w|w ∈ SNoR x} = SNoR x.
rewrite the current goal using SNoR_0 (from left to right).
We will prove {w + x|w ∈ Empty} ∪ {0 + w|w ∈ SNoR x} = SNoR x.
rewrite the current goal using Repl_Empty (λw ⇒ w + x) (from left to right).
We will prove Empty ∪ {0 + w|w ∈ SNoR x} = SNoR x.
rewrite the current goal using binunion_idl (from left to right).
We will prove {0 + w|w ∈ SNoR x} = SNoR x.
Apply set_ext to the current goal.
Let u be given.
Assume Hu: u ∈ {0 + w|w ∈ SNoR x}.
Apply ReplE_impred (SNoR x) (λw ⇒ 0 + w) u Hu to the current goal.
Let w be given.
Assume Hw: w ∈ SNoR x.
Assume H1: u = 0 + w.
We will prove u ∈ SNoR x.
rewrite the current goal using H1 (from left to right).
We will prove 0 + w ∈ SNoR x.
rewrite the current goal using IH w (SNoR_SNoS_ x w Hw) (from left to right).
We will prove w ∈ SNoR x.
An exact proof term for the current goal is Hw.
Let u be given.
Assume Hu: u ∈ SNoR x.
We will prove u ∈ {0 + w|w ∈ SNoR x}.
rewrite the current goal using IH u (SNoR_SNoS_ x u Hu) (from right to left).
We will prove 0 + u ∈ {0 + w|w ∈ SNoR x}.
An exact proof term for the current goal is ReplI (SNoR x) (λw ⇒ 0 + w) u Hu.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using L2 (from left to right).
We will prove SNoCut (SNoL x) (SNoR x) = x.
Use symmetry.
An exact proof term for the current goal is SNo_eta x Hx.
∎