An exact proof term for the current goal is HSNo_OSNo_proj0 k HSNo_Quaternion_k.