Hola,
Tengo un problema al definir la función "camino".
Si considero la definición usual de árbol binario:
Inductive AB (A:Set) : nat -> Set :=
| emptyAB : AB A 0
| forkAB : forall (h1 h2:nat), AB A h1 -> A -> AB A h2 -> AB A (S (max h1 h2)).
luego no es sencillo definir "camino" para el caso de un "forkAB", porque no se sabe en principio cuál de los sub árboles tiene la altura mayor.
Por otro lado, está la restricción del problema "La función camino debe recorrer, en el cómputo, sólo un camino del árbol."
Entonces no veo otra forma de resolver el problema que no sea agregar información a los constructores de los árboles binarios, para saber, a partir del constructor, cuál sub arbol tiene la altura mayor. Con este enfoque pude resolver el ejercicio.
¿El problema va por ahí o deberíamos ser capaces de resolverlo con la definición habitual de árboles binarios?
Saludos,
Nicolás