Refactor setup of proof equality engine for central EE (#6831)

Refactor setup of proof equality engine for central EE (#6831)

Users of an equality engine should each use the same proof equality engine that wraps it. This ensures that theory inference managers do so, by tracking the official proof equality engine for an equality engine in theory inference manager.

This is in preparation for (proper equality proofs for) central equality engine.

It also adds some debugging code that is highly useful for debugging issues related to when equalities are processed in theory inference manager.