prove all the exh-related cheats in compile_top_thm

but added a cheat for v_to_exh_extend_disjoint to do so