Buenas, realizando estas partes del ejercicio 3 quedé en una situación similar en ambos casos.
Parte 3:
Parte 5:
Estuve viendo los foros y ya apliqué case_eq (equal x a) como se sugirió, pero no se cómo seguir.
Dado que las situaciones son similares, entiendo que de resolver una parte la otra será análoga.
Saludos,
Bruno Lartigau
Hola.
No es trivial saber bien que tácticas aplicaste hasta llegar acá y si todas las definiciones que diste están bien, pero en la primera prueba podrías introducir como hipótesis MemL x (deleteAll x (consL a l)) para hacer inversión en ella (dado que MemL es inductiva y está instanciada en un constructor). Para probar False tenés IHl. Cuando quieras reducir/aplicar una definicial (como deleteAll en una hipótesis hh podés hacer simpl in hh o simpl in * para hacer reducciones en todas).
El caso de equal con false es similar y también tenés equal2.
Espero esto te ayude!
Saludos, Carlos
