Buenas!
Gracias por la respuesta. La prueba salió siguiendo esto.
De todos modos, ya habíamos intentado exactamente esto antes y el problema era que las memorias de la hipótesis inductiva quedaban fijas entonces no nos servía.
Esto lo solucionamos cambiando de lugar las variables ligadas al cuantificador (en el el enunciado del teorema) poniendo las memorias después de los naturales de modo que estas queden como variables cuantificadas al aplicar induction n1 y podamos sustituirlas para al aplicar la hipótesis.
Gracias nuevamente