An incomplete development of weight balanced trees

Eventually this will get completed and moved into HOL4 itself. Currently
supports insert, delete, union, submap, map, to_list, and comparison of
trees.
Remove spurious TODO