Apply HSNo_OSNo to the current goal.

An exact proof term for the current goal is HSNo_Quaternion_j.

∎