Apply CSNo_HSNo to the current goal.

An exact proof term for the current goal is CSNo_Complex_i.

∎