If x is a variable of type ty and M is an abstraction (with
bound variable y of type ty and body t), then ALPHA_CONV x M
returns the theorem:
where the variable x':ty is a primed variant of x chosen so
as not to be free in \y.t.
|- (\y.t) = (\x'. t[x'/y])