\DOC ALPHA_CONV

\TYPE {ALPHA_CONV : (term -> conv)}

\SYNOPSIS
Renames the bound variable of a lambda-abstraction.

\KEYWORDS
conversion, alpha.

\DESCRIBE
If {"x"} is a variable of type {ty} and {"\y.t"} is an abstraction in which
the bound variable {y} also has type {ty}, then {ALPHA_CONV "x" "\y.t"}
returns the theorem:
{
   |- (\y.t) = (\x'. t[x'/y])
}
\noindent where the variable {x':ty} is a primed variant of {x} chosen so
as not to be free in {"\y.t"}.

\FAILURE
{ALPHA_CONV "x" "tm"} fails if {x} is not a variable, if {tm} is not an
abstraction, or if {x} is a variable {v} and {tm} is a lambda abstraction
{\y.t} but the types of {v} and {y} differ.

\SEEALSO
ALPHA, GEN_ALPHA_CONV.

\ENDDOC