Support anywhere symbols

The backend does not support symbols with the anywhere attribute. These symbols are like constructors, except they do not have no-confusion axioms with certain other constructors, based on user-defined anywhere rules. Because certain no-confusion axioms are missing, we cannot unify anywhere symbols as constructors, or indeed, at all. It is not our goal to support anywhere symbols, but here is what would be required:

1. Modify the frontend to omit no-confusion axioms between pairs of symbols related by anywhere rules, but to include the others. Note that the relation between symbols is transitive, i.e. if a is related to b, and b is related to c by anywhere rules, then a is also related to c.
2. Modify the backend to recognize (from the no-confusion axioms) which constructor-like symbols are not subject to confusion, instead of requiring that all constructors be free constructors.
3. Modify the backend to emit a warning when it is asked to unify two symbols subject to confusion. The backend will already terminate with an error if the incomplete unification prevents applying a rule.
4. Eventually, if necessary, modify the frontend to emit modified no-confusion axioms based on the user-defined anywhere rules, and modify the backend to apply these as needed.
5. Eventually, if necessary, modify the backend to apply user-defined anywhere rules during unification to symbols that may be confused

Start by tracing how the frontend emits no-confusion axioms and how the backend recognizes constructor-like symbols during unification. Compare the requested handling of transitive anywhere rules, warnings for confused symbols, and eventual rule application. Done means the frontend and backend correctly support the specified anywhere-symbol cases without assuming all constructors are free constructors.