An exact proof term for the current goal is OSNo_proj1_2 0 (- k) HSNo_0 (HSNo_minus_HSNo k HSNo_Quaternion_k).