make Cv_to_ov use an alist (instead of fmap) like bv_to_ov does
get toBytecodeProofsTheory to build with new free_vars and THE