An exact proof term for the current goal is HSNo_proj0_2 0 1 CSNo_0 CSNo_1.