----------------------------------------------------------------------
GEN_PALPHA_CONV                                            (PairRules)
----------------------------------------------------------------------
GEN_PALPHA_CONV : term -> conv

LIBRARY
pair

KEYWORDS
conversion, alpha.

SYNOPSIS
Renames the bound pair of a paired abstraction, quantified term,
or other binder.

DESCRIBE
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
Drule.GEN_ALPHA_CONV, PairRules.PALPHA, PairRules.PALPHA_CONV.

----------------------------------------------------------------------