work on pushing good_v_exh up to the source level
work on compile_top_thm

reduce most of the cheat about good_v_exh, but for the remaining hole it
seems like the invariant isn't good enough.

also, define some helpers to encapsulate the value refinement relation.