Let x, y, u and v be given.

Assume Hx Hy Hu Hv.

Apply SNo_add_SNo_3c to the current goal.

Apply SNo_mul_SNo to the current goal.

An exact proof term for the current goal is Hu.

An exact proof term for the current goal is Hy.

Apply SNo_mul_SNo to the current goal.

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is Hv.

Apply SNo_mul_SNo to the current goal.

An exact proof term for the current goal is Hu.

An exact proof term for the current goal is Hv.

∎