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

LIBRARY
pair

SYNOPSIS
Creates an application of a paired abstraction from a term.

DESCRIBE
The user nominates some pair structure of variables {p} and a term {t},
and {UNPBETA_CONV} turns {t} into an abstraction on {p} applied to {p}.

   ------------------  UNPBETA_CONV "p" "t"
    |- t = (\p. t) p




FAILURE
Fails if {p} is not a paired structure of variables.

SEEALSO
PairRules.PBETA_CONV, PairedLambda.PAIRED_BETA_CONV.

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