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 (H1 (andEL p ((if p then x else y) = x) H2) ((if p then x else y) = y)).

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

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

∎