An exact proof term for the current goal is conj_CSNo_id_SNo 0 SNo_0.