This ensures that we apply top-level substitutions and rewrite bodies of
define-fun eagerly. This is required for
#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
#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 #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
#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)
```

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)
```

…ion (cvc5#11513)

This adds a macro rewrite to capture some of the rewrites in the UF
rewriter and adds proof elaboration for it, which is expected to be
accomplished by (possibly multiple steps of) alpha equivalence.

Note that it uses a more elegant solution than
cvc5#11329, which lifted APPLY_UF to
higher-order applications to ensure shadowing was eliminated. Now, the
rewriting the APPLY_UF is done "in-place", i.e. `(APPLY_UF L ts) --->
(APPLY_UF L' ts)`. As a result, we revert to a behavior where HO_APPLY
is never introduced in first order logics, making the change to TheoryUF
unecessary. It also means we don't rely on higher-order beta-reduction
in first-order logics. This reenables `alethe` on these regressions.

This rewrite is used to ensure that beta reduction does not introduce
capture avoiding substitutions. The UF rewriter is refactored to use the
reference implementation.

Adds a new utility method (getMatchConds) to node_algorith.h which will
be used for a few other pending tasks in proof elaboration.

Fills 1 proof hole in our regressions and 287 proof holes on SMT-LIB.