A good explanation is in Section `1. Eigenvariables and generic reasoning' of @inproceedings{MillerTiu, author = {Dale Miller and Alwen Fernanto Tiu}, title = {A Proof Theory for Generic Judgments: An extended abstract}, booktitle = {LICS}, year = {2003}, pages = {118-127}, url = \url{http://users.rsise.anu.edu.au/~tiu/lics03sub.pdf}, crossref = {DBLP:conf/lics/2003}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/lics/2003, title = {18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings}, booktitle = {LICS}, publisher = {IEEE Computer Society}, year = {2003}, isbn = {0-7695-1884-2}, key = {LICS}, } The section explains in which sense eigen-variables are _variables_. The paper argues, btw, for the separation of those senses and for a new quantifier to mean uniqueness only. In short, when we write forall x. forall y. body then x may well be equal to y (in body). And so, forall x. forall y. B[x,y] ====> forall z. B[z,z] OTH, when we write |nabla x. nabla y. body| then x and y are guaranteed to be different, and so the implication above no longer holds. Alwen Tiu's web page http://users.rsise.anu.edu.au/~tiu/ lists the journal version of the paper.