import Data.Vect s2 : x + sum Nil = x * fromInteger 0 s2 = Refl