PETA_CONV
PairRules.PETA_CONV : conv
Performs a top-level paired eta-conversion.
PETA_CONV maps an eta-redex \p. t p, where none of variables in the
paired structure of variables p occurs free in t, to the theorem
|- (\p. t p) = t.
Failure
Fails if the input term is not a paired eta-redex.