Hello,
I understand the reduction steps. Are you saying that the problem is that the two sets are not syntactically equal? To me this does not seem important: we just end up with two different ways to say the same thing (i.e., they are logically equivalent).
If c were mentioned in another constraint, they would not be equivalent.
How so? A concrete example would really be useful. I think that the constraint 'C [a] b d' and 'C [a] c d' are equivalent and I don't see how the rest of the context can affect this (of course I have been wrong in the past :-). The one way to see that is (like I already said) --- assume the one and prove the other and vice versa. Another way to see that is as follows: All the instances of 'C' that have '[a]' in their first argument must have the same type in the second argument otherwise the functional dependecy of 'C' will be violated. Thus 'b' and 'c' above happen to be just different names for the same thing. Yet another slightly different way to think of this is that a functional dependency is a function on types (e.g., associated type synonyms give us a way to name this function). So lets say that the functional dependecy on 'C' is called 'F'. Than we can see that both 'C [a] b d' and 'C [a] c d' are really the same thing, namely 'C [a] (F [a]) d'. -Iavor