make map_sv_def an automatic rewrite
make split_pair_match fail less often

Since this tactic is supposed to be an "enabler" rather than a test, I
think it's OK for it to be liberal and reduce to a no-op if it can't do
something.
make split_pair_match less liberal on constants

Need to at least match on the constant parts of the goal. This (and
failure in general) makes it more useful in combination with
first_assum.
fix a proof after changes to split_pair_match
work on updating exp_to_Cexp_correct