Currently, we use a set of pairs to cache responces like CompareValueComplexity(X, Y) == 0. If we had
proved that CompareValueComplexity(S1, S2) == 0 and CompareValueComplexity(S2, S3) == 0,
this cache does not allow us to prove that CompareValueComplexity(S1, S3) is also 0.
This patch replaces this set with EquivalenceClasses that merges Values into equivalence sets so that
any two values from the same set are equal from point of CompareValueComplexity . This, in particular,
allows us to prove the fact from example above.