fact: Fixpoint htree_to_btree (n:nat)(t:htree Z n){struct t} : Z_btree := match t with | hleaf _ x => Z_bnode x Z_leaf Z_leaf | hnode _ p v t1 t2 => Z_bnode v (htree_to_btree p t1)(htree_to_btree p t2) end.
imports: ZArith List Arith Bool