Let Lx, Rx, Ly, Ry, x and y be given.

Assume HLRx HLRy Hxe Hye.

Apply mul_SNoCutP_lem Lx Rx Ly Ry x y HLRx HLRy Hxe Hye to the current goal.

Assume _ H.

An exact proof term for the current goal is H.

∎