(proof-new) Arithmetic operator elim proof producing (#4783)

(proof-new) Arithmetic operator elim proof producing (#4783)

This updates the interface for arithmetic operator elimination for the new proof format.

The actual proof production of the operator elimination class (providing proofs for
introduced witness terms) will be done in a separate PR.

This also changes the witness terms introduced by this class so their body is in
Skolem form, which simplifies term formula removal.

Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>