An exact proof term for the current goal is HSNo_proj0proj1_split z w (quaternion_HSNo z Hz) (quaternion_HSNo w Hw).