Always theory-preprocess lemmas (#5817)

Always theory-preprocess lemmas (#5817)

This PR makes it so that theory-preprocessing is always called on lemmas. It simplifies the proof production in the theory preprocessor accordingly.

Additionally, it ensures that our theory-preprocessor is run on lemmas that are generated from term formula removal. Previously, this was not the case and in fact certain lemmas (e.g. literals within witness terms that are not in preprocessed form) would escape and be asserted to TheoryEngine. This was uncovered by a unit test failure, the corresponding regression is added in this PR.

It adds a new interface removeItes to PropEngine which is required for the (deprecated) preprocessing pass removeItes.

This PR now makes the lemma propery PREPROCESS obsolete. Further simplification is possible after this PR in non-linear arithmetic and quantifiers, where it is not necessary to distinguish 2 caches for preprocessed vs. non-preprocessed lemmas.