Hola.
La prueba por inducción en l1 es una opción posible.
Con las hipótesis que se ven no se puede asegurar el goal: si se aplica IHl1, tendrías que probar Mem A a l1. Al hacer inversion en H hay dos posibilidades y en una de ellas no se tendría información (a=a0). Algo falta en las hipótesis...
Volvé a mirarlo y si no sale, escribí de nuevo incluyendo las definiciones involucradas y las tácticas aplicadas hasta este punto de la prueba así vemos bien el problema y te puedo ayudar.
Saludos, Carlos