Hola, no me queda claro cómo definir que las hojas sean de un tipo distinto a los nodos internos, yo lo definí así, pero está mal, porque la foresta puede ser vacía (al ser la foresta vacía, el node puede ser una hoja):
Inductive Gtree (A B:Set) : Set :=
hoja : B -> Gtree A B
| node : A -> forest A B -> Gtree A B
with
forest (A B:Set) : Set :=
empty_f: forest A B
| add_Gtree: Gtree A B -> forest A B -> forest A B.
Saludos,
Jairo.