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 a number n and builds a fixed-height tree of height n containing integer values.

Solution