Added ewff_cmp(), slightly changed ewff_eval().

ewff_eval() now returns true if t1==t2 for EWFF_EQ. This is obviously
correct, in particular, if t1, t2 are variables.
Since ewff_true abbreviates x==x and x may not be bounded by the varmap
(for technical reasons, logically it is universally quantified, of
course), the old implementation was just correct because varmap_lookup()
deterministically returned the ((term_t) 0).