----------------------------------------------------------------------
UNBETA_CONV                                                     (Conv)
----------------------------------------------------------------------
UNBETA_CONV : term -> conv

SYNOPSIS
Returns a reversed instance of beta-reduction.

KEYWORDS
conversion.

DESCRIBE
{UNBETA_CONV t1 t2} returns a theorem of the form

   |- t2 = (\v. t') t1

The choice of {v} and the nature of {t'} depend on whether or {t1} is
a variable.  If so, then {v} will be {t1} and {t'} will be {t2}.
Otherwise, {v} will be generated with {genvar} and {t'} will be the
result of substituting {v} for {t1}, wherever it occurs.

FAILURE
Never fails.

COMMENTS
Very useful for setting up a higher-order match by hand.  The use of
{genvar} is predicated on the assumption that it will later be
eliminated through the application of the function term to some other
argument.

SEEALSO
Thm.BETA_CONV.

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