An exact proof term for the current goal is CSNo_Re2 x y (real_SNo x Hx) (real_SNo y Hy).