Fix sets cardinality inference involving equivalent parents (#6855)

Fix sets cardinality inference involving equivalent parents (#6855)

This fixes an unsoundness issue in the sets + cardinality solver.

One rule of this solver applies in sets when two parents of a child of a cardinality graph are equal, in which case we know that child or one of its siblings must be equal to the opposite parent. For example, this rule tells us that:

if T = (union T S), then (intersect T S) = S.

The explanation of this rule could consider the representative term of one the parents instead of the term itself say (union T S) is representative T, giving the unsound inference: if (union T S) = (union T S), then (intersect T S) = S. This ensures we use the original terms.

This PR also does some minor cleanup.