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