Buenas, tengo un par de consultas con respecto a este ejercicio.
Cuando pide definir la funcion ++, es necesario definir el operador infijo usando Infix o simplemente se puede utilizar la funcion append definida en el ejercicio 4.4?
Por otro lado, para demostrar l1 << l2 y l2 << l1 -> l1 = l2 defini lo siguiente:
Theorem prueba_posfijo2 : forall (A:Set) (l1 l2: list A), posfijo A l1 l2 /\ posfijo A l2 l1 -> l1 = l2.
No veo bien como arrancar, siempre genero hipotesis del tipo posfijo, pero tengo que probar igualdades sin posfijo.
Gracias.