[TYPES] Explicit renaming of bound variables

[George Cherevichenko]

 Hello.
I think I have  found "the right definition" of substitution and
alpha-conversion. Three main ideas are:
1) Contexts with multiplicity (i.e., repetitions of variables are
permitted);
2) A new form of explicit substitutions;
3) A new definition of free variables.
Renaming of bound variables when performing substitutions is done using
special reductions and may be delayed.
So far told two people: Lev Beklemishev and Mati Pentus (both like).
George.

http://arxiv.org/abs/1111.3171