Alpha-equivalence is a notion of equivalence on terms with binding structure. It captures the notion that the names of bound variables are unimportant; all that matters is the binding structure they induce.
Consider the untyped lambda-calculus.
Alpha-equivalence for terms is the least congruence relation closed under the axiom:
Alpha-equivalence generalizes in a straightforward manner to any term language with binding structure.
Twelf's notion of term equality respects alpha-equivalence; when an object-language is represented using higher-order abstract syntax, the representation enjoys alpha-equivalence for free.