prove enough of exp_to_i4_correct to be reasonably convinced

in particular, one of the pattern-match cases seems to work with
exp_to_i4_shift.

there are lots of cheats remaining (turning what was a proof based on a
simple value translation into a proof about the existence of related
values).