Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

We will prove (x + y + - z) + (z + w) = x + y + w.

rewrite the current goal using minus_SNo_invol z Hz (from right to left) at position 2.

We will prove (x + y + - z) + (- - z + w) = x + y + w.

An exact proof term for the current goal is add_SNo_minus_SNo_prop3 x y (- z) w Hx Hy (SNo_minus_SNo z Hz) Hw.

∎