La función h debe definirse recursivamente sobre un árbol (familia) de tipo ACom A n.
Fixpoint h (A:Set) (n:nat) (tree: ACom A n): nat:=
match tree with
constructor1 ... => ...
| constructor2 ... => ...
end.
Luego hay que probar que:
Lemma nombre (A:Set) : forall n:nat, forall tree : ACom A n, h A n t = pot 2 n.
Saludos, Carlos