Demore un poco porque seguí de largo. Ahora estoy retomando ejercicios salteados.
Lo anterior lo precisaba porque hacia inducción en uno de los arboles y luego de un case necesitaba probar que, si uno de los arboles era vacío y el otro no, entonces, no eran isomorfos.
Finalmente, probé hacer inducción en la relación isomorfo como recomendaste y lo resolví.
En un momento me surgió un problema similar a https://eva.fing.edu.uy/mod/forum/discuss.php?d=55952#p152958.
Tuve que cambiar en la definición de isomorfo (isomorfo A l1 r2) /\ (isomorfo A r1 l2) por (isomorfo A l1 r2) -> (isomorfo A r1 l2). Sin el cambio no me aparecían las hipótesis inductivas.
2 goals
A, B : Set
a1 : A
a2 : B
l1, r1 : bintree A
l2, r2 : bintree B
H0_ : isomorfo A B l1 l2
H0_0 : isomorfo A B r1 r2
IHisomorfo1 : isomorfo B A l2 l1 (* Solo aparece si uso -> en la definición de isomorfo *)
IHisomorfo2 : isomorfo B A r2 r1 (* Solo aparece si uso -> en la definición de isomorfo *)
______________________________________(1/2)
isomorfo B A l2 l1
______________________________________(2/2)
isomorfo B A r2 r1
No entiendo porque al usar /\ no aparecen las hipótesis inductivas. ¿No debería ser equivalente?