Hola.
En el caso inductivo va a ser necesario hacer análisis de equal (equal a x), para poder ver los casos y aplicar las definiciones correspondientes. Es útil antes de hacer análisis de casos usar remember (equal a x), para mantener la información en las hipótesis al evaluar cada caso.
Saludos, Carlos