Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions