(proof-new) Fixes for theory preprocessing proofs (#5171)

(proof-new) Fixes for theory preprocessing proofs (#5171)

This fixes several subtle issues with theory preprocessing.

The main fix is to ensure proofs are correct for cases where the theory preprocessor applies either with or without theory preprocessing (calling Theory::ppRewrite on subterms) enabled, see argument doTheoryPreprocess of preprocess. If disabled, it applies term formula removal and rewriting only. This is required for processing lemmas that are marked as "do not preprocess", which is an optimization, but is also necessary since theory combination may e.g. split on equality that was solved during ppRewrite. The solution is to use 2 separate term conversion sequences for these 2 cases.

It also fixes an issue where preprocessing is term-context-sensitive: terms underneath quantifiers are treated differently. This is now handled by a new TermContext callback "InQuantTermContext".