Simplify formalism of introduced arithmetic skolems (#8073)

Simplify formalism of introduced arithmetic skolems (#8073)

This ensures that all skolems introduced by arithmetic have concrete terms as witnesses. This avoids introducing witness terms.

This PR is important for ensuring that the "original form" of terms does not contain introduced free variables. This means that certain features (quantifier elimination, learned literals) are useful to the user. This was requested by Certora.

This also will improve proof reconstruction for extensions of non-linear arithmetic.

It also ensures that we share skolems in some cases, e.g. we use the same skolem for eliminating (div x y) and (mod x y).