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-14