Use (non-recursive) unpurified form instead of original form for defining Skolems...

Use (non-recursive) unpurified form instead of original form for defining Skolems (#8699)

This modifies our treatment of purification Skolems in the internal proof calculus. In particular, we now use an "unpurified form" instead of "original form" for defining Skolems. SKOLEM_INTRO is modified to prove the equality between a skolem and its unpurified form.

For example:
k1 purifies (ite A B C)
k2 purifies (+ k1 1)

The unpurified form of k2 is (+ k1 1), its original form is (+ (ite A B C) 1).

As a consequence:
(1) Our global skolem sharing is now slightly weaker, for example a k3 could be constructed whose unpurified form is (+ (ite A B C) 1); previously this would guaranteed to be k1.
(2) We do not require recursively computing the original form of terms when constructing purification Skolems,
(3) The witness form proof generator requires a fix point.
(4) The LFSC signature is simplified, and does not require a side condition to recursively compute the original form of a Skolem.

Fixes cvc5/LFSC#81.