Je n'avais pas regardé le code quand j'ai répondu, mais oui, c'est normal comme comportement vu que c'est exactement ce qui se passe avec les quantificateurs (que ça soit en logique du premier ordre ou dans des autres supérieurs).
Cela dit, je crois que ça doit mener à des bugs bien cons et difficilement identifiables, parce que ce n'est pas forcément intuitif (je crois que si la question n'était pas orientée, je n'aurai pas prêté attention à ce comportement).