Hola.
Acoto algo más.
Es un buen ejercicio para usar el resultado de inverse_image, considerando que la relación menor entre naturales es bien fundada (lt_wf).
Al probar que la relación elt entre árboles (un árbol es menor que otro si tiene menos nodos) es bien fundada, habilitaría a usar este orden para justificar la terminación de una función sobre árboles que no sea definida por recursión estructural (con Fixpoint). Para justificar su terminación habría que ver que los árboles en las llamadas recursivas tienen menos nodos que el árbol parámetro (pero esto no se pide en el ejercicio).
Saludos, Carlos