Primero que nada me tira un error la definición de "++" porque ya está definido para listas ese chirimbolo. De momento estoy usando "+++" para avanzar pero qué recomiendan hacer para que quede más prolijo?
Segundo, una pregunta más en general pero que aplica también al ejercicio seis en particular. A todas las igualdades a demostrar les tiro con reflexivity y salen en un paso. Tal vez la idea era que hiciésemos otra cosa un poco más elaborada o tal vez está bien, no sé.
Saludos!