induction on the structure of the first argument that the tree
resulting from `bind u f` is a tree with the same strucure as `u`,
except that each leaf `a` has been replaced with `fa`:
\tree (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5)))
<pre>
induction on the structure of the first argument that the tree
resulting from `bind u f` is a tree with the same strucure as `u`,
except that each leaf `a` has been replaced with `fa`:
\tree (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5)))
<pre>