UNPBETA_CONV
PairRules.UNPBETA_CONV : (term -> conv)
Creates an application of a paired abstraction from a term.
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.