Let x, y and z be given.

Assume Hx Hy Hz.

Apply SNo_mul_SNo to the current goal.

An exact proof term for the current goal is Hx.

Apply SNo_mul_SNo to the current goal.

An exact proof term for the current goal is Hy.

An exact proof term for the current goal is Hz.

∎