start on making compiler proofs use new v_to_exh relation

looks promising, but haven't covered the hard parts yet