Use function array constants in HO solver (#8818)

Use function array constants in HO solver (#8818)

This makes lambdas rewrite to function array constants when possible. This extends our HO solver and utilities to be robust to check whether a node represents a lambda (uf::FunctionConst::toLambda).

This furthermore removes the isConst rule for LAMBDA; lambdas are never constant.

The PR also improves our check-model so that warnings are not thrown if rewriting can show that the model value of a term is equivalent modulo rewriting to its representative in the model equality engine.

This eliminates the last remaining static calls to rewrite. This is work towards eliminating SmtEngineScope.