GEN_PALPHA_CONV : term -> conv
STRUCTURE
LIBRARY
pair
SYNOPSIS
Renames the bound pair of a paired abstraction, quantified term, or other binder.
DESCRIPTION
The conversion GEN_PALPHA_CONV provides alpha conversion for lambda abstractions of the form \p.t, quantified terms of the forms !p.t, ?p.t or ?!p.t, and epsilon terms of the form @p.t.

The renaming of pairs is as described for PALPHA_CONV.

FAILURE
GEN_PALPHA_CONV q tm fails if q is not a variable, or if tm does not have one of the required forms. GEN_ALPHA_CONV q tm also fails if tm does have one of these forms, but types of the variables p and q differ.
SEEALSO
HOL  Kananaskis-13