generalize hits max rec depth when ground exponentials are present

[kim-em]

example (a : Nat) : ((2 ^ 7) + a) - 2 ^ 7 = 0 := by
  generalize 0 - 0 = x -- fails with a max rec depth error (should do nothing)

Observed on both master and v4.6.0-rc1.

Reducing 7, changing either - to a +, or removing the + a or changing it to a constant, all work.