write section 3 (and create a new section 4) that introduces the
library via the Braun tree 'insert' function
add an abstract
add a little bit more to the coq parser
started on copy_insert
update TODO