# 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

Look at this file

Going home

Pierre Castéran