An exact proof term for the current goal is CSNo_HSNo_proj0 1 CSNo_1.