make less noisy
minor cleanups

mostly to make there be a simply stated theorem with lemmas
Adding size.v from class
Added alternate implementation of Braun trees
Counting copy

Proof not finished, contains what was worked out in class.
Rewrote copy2 to look more like the definition in the braun tree paper. It could still use some work though. It currently uses to nested lets to bind the valus for m, s, and t, which looks ugly. And the Lemma's used to solve the obligations on copy2 could probably be cleaned up a little.
Added newline to end of copy.v
remove unused lemma
Beginnings of the various make_array algorithms.
remove extraneous parens
some progress: trying to do things by odds and evens instead
of all at once on non-zero nats
show thing that fails (but now it fails slowly, which suggest it isn't obviously stupid)
get everything else working

... except the lemmas that say how copying_copy
    unfolds (which are Admitted)
A different approach to proving the timing

relies crucially on the "hidden" nature of the "Time"
constructor; if that were available, times could be "forged"
but we can just refrain from using it directly, I guess.
break out monad2.v
copy works!!
refactor to pull out fl_log into its own library
remove some ugly "S"s from insert

same trick causes Program to ask me to prove false
things for copy, tho, sadly.
Implement naive make_array 1