The Barendregt convention is a standard practice informal proofs about either the -calculus or programming languages with binding constructs. It is the practice of dealing -convertible terms as essentially equal.
In particular, the Barendregt convention assumes that we are able to rename terms regularly when pushing substitutions under binder, as much as it is convenient. This avoids the two usual problems:
The exact wording is as follows [Barendregt 1984, p. 26]:
2.1.13 . If , ..., occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free variables.
The convention is named after Henk Barendregt, who uses it throughout his book [Barendregt 1984]. However, in the addenda of the sixth reprinting, Barendregt attributes it to James Ottman:
The variable convention (keeping the names of bound variables as much different as convenient from those of the free variables) is used throughout the book and is convenient in an informal precise setting. This method was brought to my attention by Thomas Ottman in 1972 and ever since I used it without referring to him (as it is so natural). After the appearance of this book the convention became baptized with my name. This is unjustified to Ottman and for this reason I mention explicitly his name in these corrections.