Hola, veo que este ejercicio se preguntó varias veces pero leyendo lo que se publicó anteriormente no me está saliendo todavía.
Arranqué haciendo inducción en la lista y después hice eq_case como es natural.
Con lo que no estoy pudiendo es con el caso en que equal x a = false.
X : Set x0 : X xs : List x : X H : MemL x (x0 ::' delete x xs) IHxs : isSet xs -> MemL x (delete x xs) -> False H0 : isSet xs H1 : MemL x0 xs -> False H2 : equal x x0 = false ______________________________________(1/1) MemL x (delete x xs)
De momento tengo esto. Tienen alguna recomendación de cómo seguir?
Traté de hacer un cut (x0 ::' delete x xs = delete x xs) pero se termina poniendo difícil eso también.