An exact proof term for the current goal is CSNo_Im2 0 1 SNo_0 SNo_1.