WFFEQ-AB-ETA : WFFOPWFFEQ-AB-ETA is a wff operation.
Verifies that wff1 and wff2 are equal up to
lambda-normalization with eta rule only, and alphabetic change of
bound variables. (Compare WFFEQ-AB-BETA, WFFEQ-AB-LAMBDA.)
The calling scheme for WFFEQ-AB-ETA is:
(WFFEQ-AB-ETA WFF1 WFF2)
The result is of type BOOLEAN.
The arguments have the following meaning:
WFF1 : old wff
WFF2 : new wff
TPS documentation homepage