An exact proof term for the current goal is If_i_0 (0 ≤ x) x (- x) Hx.