tree that is ready to accept any `int -> int` function and produce the
updated tree.
+\tree (. (. (f 2) (f 3)) (. (f 5) (. (f 7) (f 11))))
\f .
_____|____
resulting from `bind u f` is a tree with the same strucure as `u`,
except that each leaf `a` has been replaced with `f a`:
-\tree (. (fa1) (. (. (. (fa2)(fa3)) (fa4)) (fa5)))
+\tree (. (f a1) (. (. (. (f a2) (f a3)) (f a4)) (f a5)))
. .
__|__ __|__
we'll give an example that will show how an inductive proof would
proceed. Let `f a = Node (Leaf a, Leaf a)`. Then
-\tree (. (. (. (. (a1)(a2)))))
-\tree (. (. (. (. (a1) (a1)) (. (a1) (a1))) ))
+\tree (. (. (. (. (a1) (a2)))))
+\tree (. (. (. (. (a1) (a1)) (. (a1) (a1)))))
.
____|____