Tengo un problema desagradable con la formalización de un teorema que usa un tipo de datos que tiene algunos constructores cuyos índices tienen concatenación de listas. Cuando intento usar el modo emacs para dividir mayúsculas y minúsculas, Agda devuelve el siguiente mensaje de error:

I'm not sure if there should be a case for the constructor
o-success, because I get stuck when trying to solve the following
unification problems (inferred index ≟ expected index):
  e₁ o e'' , x₁ ++ x'' ++ y₁ ≟ e o e' , x ++ x' ++ y
  suc (n₂ + n'') , x₁ ++ x'' ≟ m' , p''
when checking that the expression ? has type
suc (.n₁ + .n') == .m' × .x ++ .x' == p'

Dado que el código tiene más de un pequeño número de líneas, lo pongo en la siguiente esencia:

https://gist.github.com/rodrigogribeiro/976b3d5cc82c970314c2

Cualquier consejo es apreciado.

Mejor,