Unless I’m mistaken, priority doesn’t matter for leq as defined above?
Normally CHR will try rules in listed order but for most rule sets even this doesn’t matter. It’s usually a good idea to code so that order of rule selection is irrelevant although it can be convenient to have simplifying rules happen before complicating rules, to reduce algorithm complexity.