Use-case for folds/attribute grammars: efficient rename decision procedure

[jaccokrijnen]

Deciding appears_free_in v t, which is used in no_capture in the rename relation, requires traversing the whole term t, which results in quadratic run-time when checked throughout the AST.

A more efficient approach would be to maintain a set of free variables in the sub-term, and compute that recursively (synthesized). Deciding can then be done in terms of that set. This approach does require an equivalence between appears_free_in v t and In v (fv t) to construct the soundness proof.

[jaccokrijnen]

Same problem in Unique: need to decide ~ bound_in for every binder