An exact proof term for the current goal is SNo_add_SNo_3 x y (z + w) Hx Hy (SNo_add_SNo z w Hz Hw).