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