Let x, y, z and w be given.

Assume Hx Hy Hz Hw.

rewrite the current goal using add_SNo_assoc (x + y) z w (SNo_add_SNo x y Hx Hy) Hz Hw (from left to right).

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

rewrite the current goal using add_SNo_com_3b_1_2 x y z Hx Hy Hz (from left to right).

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

Use symmetry.

An exact proof term for the current goal is add_SNo_assoc (x + z) y w (SNo_add_SNo x z Hx Hz) Hy Hw.

∎