prove compile_top_divergence, cheating on modules cases

haven't proved anything about compile_decs (required for modules).
but the top-level declarations stuff is shaping up pretty nicely.