Hola.
No entiendo por qué hacés "case t1; case t2;simpl;constructor;constructor."
Si ponés "constructor; assumption." queda probado el lema. Notar que assumption en este caso corresponde a usar la hipótesis inductiva.
Saludos, Carlos
pd: Tratá de plantear las dudas sin incluir mucho código.