Buenas, estoy trancado en este ejercicio. Para comenzar la prueba apliqué aplique intros y luego induction en t. La prueba para t = emptybintree A sale, pero para el caso de Node no.
Para el otro caso tomo como testigo a (node A a t2 t1) y luego de aplicar constructor llego a lo siguiente:
2 subgoals
A : Set
a : A
t1, t2 : bintree A
IHt1 : {t' : bintree A | mirror A t1 t'}
IHt2 : {t' : bintree A | mirror A t2 t'}
______________________________________(1/2)
mirror A t1 t1
______________________________________(2/2)
mirror A t2 t2
Probé eliminando IHt1 pero no veo como me podría ayudar. Alguna sugerencia?
Gracias.