Practico 5 - Ej 5.3.5

Practico 5 - Ej 5.3.5

de Carlos Augusto Rodriguez Gonzalez -
Número de respuestas: 1

Hola,

Estoy trancado con este ejercicio, trate de probar el siguiente lemma que creo me seria util: 

Lemma redMem: forall (l:List) (x a:A), ~(equal x a = true) /\ MemL x (consL a l) -> MemL x l.

Pero siempre quedo estancado en algo asi:

inversion_clear H1.

constructor.

constructor.

apply IHl.

constructor.

apply IHl.

...


Alguna sugerencia de como encar esta ultima prueba o el ejercicio en general?


Gracias de antemano.



En respuesta a Carlos Augusto Rodriguez Gonzalez

Re: Practico 5 - Ej 5.3.5

de Carlos Luna -

Hola.

Deberías reflejar el efecto de inversión sobre la hipótesis MemL x (consL a l) en la hipótesis equal x a <> true, usando:

inversion_clear H1 in H...

o hacer inversion en vez de inversion_clear para que te deje la igualdad para x y a.

Saludos, Carlos