Added a rewrite for iff:
x = c iff x = d ---> false
This fixes Andy's problem if unconstrained simplification is turned on.