prove row_to_i4_shift and exp_to_i4_shift

turns out the statement was almost right before, just needed to
strengthen the hypotheses slightly.