Hola; La linea que define:
Infix "++" := Plus (left associativity, at level 94), no me compila en coqide; me da el sigiente error:
Error: Notation _ ++ _ is already defined at level 60 with arguments
at next level, at level 60 while it is now required to be at level 94
with arguments at level 94, at next level.
Lo que hice fue cambiarle el nombre (uso +++), está bien?