Improving equality engine tracing (#4770)

Improving equality engine tracing (#4770)

To keep track of the reasoning in the equality engine for n-ary kinds, for which partial applications amount to valid fully-applied terms, it's imperative to be able to see the IDs of the internal representation of the equality engine nodes. This commit updates tracing messages to print these IDs. It also improves the tracing for explanation generation.