ALPHA : term -> term -> thm
STRUCTURE
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
HOL  Kananaskis-13