An exact proof term for the current goal is OSNo_proj0_2 0 (- j) HSNo_0 (HSNo_minus_HSNo j HSNo_Quaternion_j).