bug(parikh_image): repair overrestrictive optimisation

Optimisation was requiring that, if a label may have n different
characters, then each of the n characters are different in two ways:

1. char(i) < char(i+1) (for some ordering of char vars)
2. there was some difference in predicate satisfaction between char(i)
   and char(i+1).

This fails when there is only one possible satisfying character for the
label. Then we cannot have two characters that are the same but also
different.

Relax optimisation so that

1. char(i) < char(i+1) OR the count of characters of char(i+1) is 0,
2. same for predicate satisfaction (only differ if count > 0),
3. if count(i) is 0, then so is count(i+1).