An exact proof term for the current goal is OSNo_proj0_2 x y (quaternion_HSNo x Hx) (quaternion_HSNo y Hy).