An exact proof term for the current goal is CSNo_HSNo_proj1 i CSNo_Complex_i.