395-2013 This repo contains Coq code for functions from Chris Okasaki's paper: Three algorithms on Braun trees Journal of Functional Programming Volume 7 Issue 6, November 1997, 661 - 666 pdf from citeseer