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