An exact proof term for the current goal is SNo_Im 1 SNo_1.