prove compile_top_divergence

(depending on a cheated not_evaluate_decs_timeout theorem which probably
needs the semantics to be tweaked.)