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.