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.
∎