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