Buenasss, estoy hace rato dandole vueltas a este ejercicio, es el último que me queda y no logro resolver los goals para el caso equal x a = false.
Para llegar hasta aquí, lo que hice fue inducción en l, probé el paso base, e hice case_eq equal x a. El caso = true lo probé sin problemas.
Pero para este caso, aplicando IHl me queda por probar MemL x (delete x l), y puedo ver cómo en la teoría, dadas estas hipótesis, MemL x (delete x l) es verdadero, pero no estoy pudiendo probarlo.
Tal vez el problema está en mi definición de delete:
Fixpoint delete (a: A) (l : List) {struct l} : List :=
match l with
| nullL => nullL
| consL elem t =>
match equal a elem with
| true => t
| false => consL elem (delete a t)
end
end.
Muchas gracias!