(proof-new) proofs for ArithCongMan -> ee facts (#5207)

(proof-new) proofs for ArithCongMan -> ee facts (#5207)

Threads proof production through the ArithCongruenceManager's pipeline
of information to the equality engine.

The idea is to define a method:

ArithCongruenceManager::assertLitToEqualityEngine(literal, reason, pf)
This method asserts a literal to the equality engine with the given
proof and reason. It stores the proof of the literal for the equality
engine's future reference, and is smart about symmetric literals.

This machinery uses proofs that are not closed over the reason, as the
equality engine requires.

Other functions in the pipeline:

assertionToEqualityEngine
equalsCostant
construct proofs and call assertLitToEqualityEngine.
Future commits will address the ee -> ArithCongruenceManager pipeline,
and the relationship between ArithCongruenceManager and the rest of
arithmetic.