Let x and y be given.

Assume Hx Hy.

Apply mul_SNo_prop_1 x Hx y Hy to the current goal.

Assume H _ _ _ _.

An exact proof term for the current goal is H.

∎