Para demostrar que sum.(xs ++ ys) = sum.xs + sum.ys, necesitamos tener las definiciones escritas:

(++) : [A] → [A] → [A]
[ ]
++ ys ≐ ys
(x ▷ xs)
++ ys ≐ x ▷ (xs ++ ys)

sum : [Num] → Num
sum.[ ]
0
sum.(x ▷ xs)
x + sum.xs

Prueba 1: por inducción en xs

Caso Base: reemplazo la variable elegida por [ ]:

sum.([ ] ++ ys) = sum.[ ] + sum.ys

y pruebo lo que obtengo:

      sum.([ ] ++ ys)
={ Definición de ++}
      sum.ys
={ Aritmética }
      
0 + sum.ys
={ Definición de sum }
      sum.[ ] + sum.ys

Caso inductivo: Copio el teorema tal como venía, y le llamo Hipótesis Inductiva (HI):

(HI) sum.(xs ++ ys) = sum.xs + sum.ys

reemplazo ahora (x ▷ xs) en lugar de xs en todos lados:

sum.((x ▷ xs) ++ ys) = sum. (x ▷ xs) + sum.ys

y demuestro lo que obtuve usando las definiciones y la HI.

      sum.((x ▷ xs)++ ys)
={ Definición de ++}
      sum.( x ▷ (xs ++ ys))
={ Definición de sum }
      x +
sum.(xs ++ ys)
={ HI }
      
x + sum.xs + sum.ys
={ Definición de sum }
      sum.(x ▷ xs) + sum.ys

Prueba 2: Puede ocurrir que no se nos ocurran algunos pasos de la demostración de arriba, así que hay otra forma de escribir esta prueba, un poco más repetitiva pero que hace más fácil imaginarse qué hacer. Por lo demás, la prueba es la misma (también por inducción).

Caso Base: sum.([ ] ++ ys) = sum.[ ] + sum.ys

En vez de salir de un lado y llegar al otro, tomo todo.

      sum.([ ] ++ ys) = sum.[ ] + sum.ys
≡{ Definición de ++}
      sum.ys =
sum.[ ] + sum.ys
≡{ Definición de sum }
      sum.ys= 0 + sum.ys
≡{ Aritmética }
      True

Caso inductivo: Usando

(HI) sum.(xs ++ ys) = sum.xs + sum.ys

pruebo:

sum.((x ▷ xs) ++ ys) = sum. (x ▷ xs) + sum.ys.

Tomo todo y opero:

      sum.((x ▷ xs)++ ys) = sum. (x ▷ xs) + sum.ys
≡{ Definición de ++}
      sum.( x ▷ (xs ++ ys)) = sum. (x ▷ xs) + sum.ys
≡{ Definición de sum }
      x +
sum.(xs ++ ys) = sum. (x ▷ xs) + sum.ys
≡{ HI }
      x + sum.xs + sum.ys =
sum. (x ▷ xs) + sum.ys
≡{ Definición de sum }
      x + sum.xs + sum.ys = x + sum.xs + sum.ys
≡{ Reflexividad de = }
      True