slight reorg. and improved print_bv_list_print_envE

state the print_bv_list theorem in terms of the v_bv relation, since
that's what we ought to be establishing in compile_top_thm
bit more compile_top_thm

tried to establish v_bv for the new top-level variables, but had to
cheat away problems with the new exh.