Hola.
Si, pueden hacerlo. No obstante, se están complicando mucho.
Recuerden que al hacer inducción no solo se puede razonar sobre una lista en este caso, sino también sobre (posfijo A l1 l2), que es un objeto inductivo. Mi consejo es que prueben hacer inducción en la hipótesis referida (luego de hacer intros).
El caso base sale fácil y para el caso inductivo tengan presente que van a tener que probar un existe pero la hipótesis inductiva es también un existe. En este caso tienen primero que usar (eliminar) la hipótesis inductiva antes de proponer el testigo para el goal. La prueba sale fácil, sin ser necesario usar lemas auxiliares.
Saludos, Carlos