An exact proof term for the current goal is OSNo_I 0 (- i) HSNo_0 (HSNo_minus_HSNo i HSNo_Complex_i).