make some unused pattern variables underscores
prove row_to_i4_acc

tweak the definition to make it true
reduce exp_to_i4_shift to a cheated row_to_i4_shift

but the latter looks like it might be false as stated