Let P, x and y be given.

Assume HxS: SNo x.

Assume HyS: SNo y.

Apply (xm P) to the current goal.

Assume HP.

rewrite the current goal using (If_i_1 P x y HP) (from left to right).

An exact proof term for the current goal is HxS.

Assume HnP.

rewrite the current goal using (If_i_0 P x y HnP) (from left to right).

An exact proof term for the current goal is HyS.

∎