declare that copy_log is done

I didn't do anything more than prove the braun invariant for
correctness. One might want to prove that, for all n less
than the size, indexing into the tree returns the
argument to copy, but the polymorphic type on copy
guarantees that in a way that makes me think we don't need
to bother.