Trees with fixed height

Here is a type of fixed height tree.

Inductive htree (A:Set) : nat->Set :=
 | hleaf : A->htree A 0
 | hnode : forall n:nat, A -> htree A n -> htree A n -> htree A (S n).

We say that a value of type htree A n is a tree of height n. Define a function that takes any natural number h and builds a perfect fixed-height tree of height h containing pairwise different integer values.

Solution