Hola,
Llegué a lo mismo que la solución para la demostración del caso inductivo, con dos casos posibles. Para el caso de que saca0(w) distinto de cero, lo probé de otra forma que me parece mas sencilla a la mostrada en la solución y por eso quiero saber si es correcta.
eval(saca0(wx))= (def saca0)
eval(saca0(w)x)= (def eval)
eval(saca0(w))*10 + x= (hip. ind.)
eval(w)*10 + x= (def. eval)
eval(wx)
Muchas gracias!