Let p, x and y be given.

Apply (xm p) to the current goal.

Assume H1: p.

Apply orIL to the current goal.

An exact proof term for the current goal is (If_i_1 p x y H1).

Assume H1: ¬ p.

Apply orIR to the current goal.

An exact proof term for the current goal is (If_i_0 p x y H1).

∎