finish non-pattern-match cases of exp_to_i4_shift

but haven't yet updated the proofs for the new IL4 with sequencing
thoughts towards saying row_to_i4 treats bvs like an accumulator

it's not quite true because it can clobber the top element; also the
definition of row_to_i4 on the "should not happen" cases probably needs
to change to make this true.