Eliminate shadowing in the quantifiers rewriter (#8244)

Eliminate shadowing in the quantifiers rewriter (#8244)

Fixes #8227.

Recently, we allowed unevaluatable terms to be in the range of substitutions solved during preprocess.

In very rare cases, it may be the case that a quantified formula is substituted into itself, e.g.:
forall x. P(x, b) where b was solved to be forall x. P(x, c)
This leads to forall x. P(x, forall x. P(x, c)) where x is shadowed.

To resolve this issue, we eliminate shadowing in the quantifiers rewriter, e.g. we rewrite the above to forall x. P(x, forall y. P(y, c)).

An alternative solution would be to ensure we use capture avoiding substitutions, but this severely complicates our usage of substitutions throughout the preprocessor / proof system.

This PR also eliminates some dead code in the quantifiers rewriter.