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