Binary tree and RBMaps

In this file we define Tree.ofRBNode. This definition was moved from the main file to avoid a dependency on RBMap.

TODO

Implement a Traversable instance for Tree.

References

https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html