Monomorphic binary trees and polymorphic trees

Here is a monomorphic type of binary trees:

Inductive Z_btree : Set :=
  Z_leaf : Z_btree | Z_bnode : Z->Z_btree->Z_btree->Z_btree.

Build the type btree of polymorphic binary trees. Define translation functions from Z_btree to btree Z and vice versa. Prove that they are inverse to each other.

Solution