Frame equalities: a to that uses a named set's function (phase(this) == phase(other)) still gets the frame #506

Problem. Since #498, a to can refer to a named state set through its function, for example undo(this) == undo(old(this)) or phase(this) == phase(other). AuxStateHandler.getMissingStates only counts a set as mentioned when one of its states appears in to. A set used through its function still gets the frame phase(this) == phase(old(this)). For to = "phase(this) == phase(other)" that frame contradicts the spec, unless other happened to be in the same state.

Constraint. Counting every application as a mention is wrong as well. to = "phase(this) == phase(this)" keeps the set today, because the frame is added, and must keep doing so. The rule has to count an application only when it constrains the post-state receiver. That is the same question #504 asks about states.

Split out of #502, whose phase(this) == open form becomes the state shorthand before the frame logic runs and does not depend on this.