fix(UF): Use appropriate explanation in up_uf_rs

[bclement-ocp]

Functions apply_sigma_uf and up_uf_rs are used to update the internal state of the union-find when applying a substitution sigma (a substitution ((p, v, ex) as sigma) represents the substitution p := v with justification ex).

The first function, apply_sigma_uf, is responsible for actually applying the substitution p := v. The second function, up_uf_rs, is responsible for computing normal forms w.r.t. AC rules once the substitution p := v has been applied.

When up_uf_rs finds new representatives, it currently adds them with the explanation justifying p := v, but this is not enough to actually ensure the equality between the old and new representative: it can depend on arbitrary explanations picked up by in the environment by the call to normal_form env rr.

This patch changes up_uf_rs to add the proper explanation in neqs_to_up.

[bclement-ocp]

Actually this case might be covered by the use of explain_repr_of_distinct? Marking as draft until I investigate further.