ALPHA
Thm.ALPHA : term -> term -> thm
Proves equality of alpha-equivalent terms.
When applied to a pair of terms t1 and t1' which are
alpha-equivalent, ALPHA returns the theorem |- t1 = t1'.
------------- ALPHA t1 t1'
|- t1 = t1'
Failure
Fails unless the terms provided are alpha-equivalent.