What is Type_equal for?
The "missing" graph datatype was invented in the '70s
How does foldr/build elimination work?
Binary search, revisited
Binary search with confidence