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.