This ensures that we apply top-level substitutions and rewrite bodies of
define-fun eagerly. This is required for
cvc5#11513.

In particular, currently, due to the fact that variables are *not*
fresh, and the rewriter does not rewrite inside of operators, beta
redexes could appear arbtirarily nested in APPLY_UF. As a result, we
were requiring the fairly sophisticated "shadow elimination" methods for
handling benchmarks such as:
```
(define-fun P ((x Int)) Bool false)
(define-fun Q ((x Int)) Bool (P x))
(assert (Q 0))
(check-sat)
```

In particular, `Q` would be defined to be the lambda `(lambda ((x Int))
(@ (lambda ((x Int)) false) x))`, which assuming the rewriter does not
rewrite inside of operators, leads us to requiring shadow elimination to
do beta reduction.

We previously made a nested call from within the rewriter to ensure such
shadowing was resolved prior to beta reduction. The PR
cvc5#11329 refactored this so that beta
redexes for non-rewritten lambdas were lifted to HO terms so that the
rewriter could track proofs without being self referential. However, as
a downside, we now require HO reasoning in first order logics, in
particular, lambdas could be rewritten and beta reduction could be done
for HO applications. The PR cvc5#11513
addresses this shortcoming by allowing non-rewritten lambdas to be
beta-reduced. However, proof elaboration fails since this requires
arbitrarily nested shadow elimination. In particular, a proof of the
above benchmark would (unintuitively) introduce shadowing elimination +
alpha equivalence.

The solution is to apply top-level substitutions + rewriting to *bodies*
of lambdas as they are defined. this prevents HO rewriting while
eliminating complications due to shadowing in beta redexes.

We do not rewrite defined constants, since this complication does not
arise and it better to be lazy based on some benchmarks in SMT-LIB
(cpachecker in QF_UFLRA).

There are several motivations for this change:
1. It makes the proofs significantly simpler and resolves all open
issues related to define-fun (after
cvc5#11513 is merged),
2. It makes the output of e.g. `-o post-asserts` much more intuitive. In
particular, prior to this commit, we'd get:
```
(set-logic ALL)
(define-fun Q ((x Int)) Bool (@ (lambda ((x Int)) false) x))
(define-fun P ((x Int)) Bool false)
(assert false)
(check-sat)
```
whereas now we get:
```
(set-logic ALL)
(define-fun Q ((x Int)) Bool false)
(define-fun P ((x Int)) Bool false)
(assert false)
(check-sat)
```

This ensures that we apply top-level substitutions and rewrite bodies of
define-fun eagerly. This is required for
cvc5#11513.

In particular, currently, due to the fact that variables are *not*
fresh, and the rewriter does not rewrite inside of operators, beta
redexes could appear arbtirarily nested in APPLY_UF. As a result, we
were requiring the fairly sophisticated "shadow elimination" methods for
handling benchmarks such as:
```
(define-fun P ((x Int)) Bool false)
(define-fun Q ((x Int)) Bool (P x))
(assert (Q 0))
(check-sat)
```

In particular, `Q` would be defined to be the lambda `(lambda ((x Int))
(@ (lambda ((x Int)) false) x))`, which assuming the rewriter does not
rewrite inside of operators, leads us to requiring shadow elimination to
do beta reduction.

We previously made a nested call from within the rewriter to ensure such
shadowing was resolved prior to beta reduction. The PR
cvc5#11329 refactored this so that beta
redexes for non-rewritten lambdas were lifted to HO terms so that the
rewriter could track proofs without being self referential. However, as
a downside, we now require HO reasoning in first order logics, in
particular, lambdas could be rewritten and beta reduction could be done
for HO applications. The PR cvc5#11513
addresses this shortcoming by allowing non-rewritten lambdas to be
beta-reduced. However, proof elaboration fails since this requires
arbitrarily nested shadow elimination. In particular, a proof of the
above benchmark would (unintuitively) introduce shadowing elimination +
alpha equivalence.

The solution is to apply top-level substitutions + rewriting to *bodies*
of lambdas as they are defined. this prevents HO rewriting while
eliminating complications due to shadowing in beta redexes.

We do not rewrite defined constants, since this complication does not
arise and it better to be lazy based on some benchmarks in SMT-LIB
(cpachecker in QF_UFLRA).

There are several motivations for this change:
1. It makes the proofs significantly simpler and resolves all open
issues related to define-fun (after
cvc5#11513 is merged),
2. It makes the output of e.g. `-o post-asserts` much more intuitive. In
particular, prior to this commit, we'd get:
```
(set-logic ALL)
(define-fun Q ((x Int)) Bool (@ (lambda ((x Int)) false) x))
(define-fun P ((x Int)) Bool false)
(assert false)
(check-sat)
```
whereas now we get:
```
(set-logic ALL)
(define-fun Q ((x Int)) Bool false)
(define-fun P ((x Int)) Bool false)
(assert false)
(check-sat)
```