GEN_PALPHA_CONVPairRules.GEN_PALPHA_CONV : term -> convRenames the bound pair of a paired abstraction, quantified term, or other binder.
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.
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.
Drule.GEN_ALPHA_CONV,
PairRules.PALPHA, PairRules.PALPHA_CONV