Implement the exclusive disjunction on booleans
Implement a boolean equality test on natural numbers
Define an inductive type for binary trees (without labels)
Define a function counting the number of nodes in a tree
Define a tree with one node, with three nodes, and test your size function
Define a function counting the depth of the tree. Hint: you can use the function maxn : nat -> nat -> nat to compute the maximum of two natural numbers. Then test your depth function.
State and prove that the height is smaller than the number of nodes.