An exact proof term for the current goal is HSNo_OSNo_proj1 j HSNo_Quaternion_j.