ALPHA : term -> term -> 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 CONDITIONS
Fails unless the terms provided are alpha-equivalent.

EXAMPLE
  # ALPHA `!x:num. x = x` `!y:num. y = y`;;
  val it : thm = |- (!x. x = x) <=> (!y. y = y)

  # ALPHA `\w. w + z` `\z'. z' + z`;;
  val it : thm = |- (\w. w + z) = (\z'. z' + z)

SEE ALSO
aconv, ALPHA_CONV, GEN_ALPHA_CONV.