Let p, x and y be given.

Assume H1: p.

Apply (If_i_correct p x y) to the current goal.

Assume H2: p ∧ (if p then x else y) = x.

An exact proof term for the current goal is (andER p ((if p then x else y) = x) H2).

Assume H2: ¬ p ∧ (if p then x else y) = y.

An exact proof term for the current goal is (andEL (¬ p) ((if p then x else y) = y) H2 H1 ((if p then x else y) = x)).

∎