[proofs] Generalize handling of constants merged in equality engine (#8781)

[proofs] Generalize handling of constants merged in equality engine (#8781)

Previously the reconstruction of EUF proofs was not considering a corner case from the equality engine where it infers that two constants are disequal from other equalities, but these other equalities all become of the form x = x at the time we are explaining this disquality. In this case the constant disequality is justified with MERGED_THROUGH_CONSTANTS rather than MERGED_THROUGH_TRANS as other disequalities.