ALPHA : term -> term -> thm
STRUCTURE
Thm
SYNOPSIS
Proves equality of alpha-equivalent terms.
DESCRIPTION
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.
SEEALSO
aconv, ALPHA_CONV, GEN_ALPHA_CONV
HOL  Kananaskis-13