LamTerm.betaBounded bug

[JOSHCLUNE]

Currently, LamTerm.betaBounded may not fully beta reduce an expression regardless of how large an n it is given. This interacts poorly with LamTerm.betaReduceHacky and LamTerm.betaReduceHackyIdx, making it possible for auto's preprocessing to run into an infinite loop.

One example of this occurring can be seen in this theorem:

set_option auto.smt false in
set_option auto.tptp true in
set_option auto.native true in
theorem test {f : α → β} (P : (α → γ) → Prop)
  (symbol1 : β → γ) (symbol2 : β → β)
  (h : P ((symbol1 ∘ symbol2) ∘ f)) : False := by
  auto [h, Function.comp_def] -- This should fail quickly rather than infinitely loop

There are presumably multiple ways to resolve this issue, but one simple way that I believe should work would be to change the last line of LamTerm.betaBounded from LamTerm.mkAppN fn argsb to (LamTerm.mkAppN fn argsb).betaBounded n' (and update the theorems LamTerm.maxEVarSucc_betaBounded and LamEquiv.ofBetaBounded accordingly).