Given an equality of the form (C x1 ... xn = C y1 ... yn),
generate an product of the equalities (x1 = y1) ... (xn = yn).
The equalities are let-bound to the provided name.
the equality to exploit injectivity on
the name at which to bind the result