prove evaluate_decs_closed
finish proving compile_top_thm

required tweaking the invariant and statement slightly to cope with
modules properly