1\DOC
2
3\TYPE {UNBETA_CONV : term -> conv}
4
5\SYNOPSIS
6Returns a reversed instance of beta-reduction.
7
8\KEYWORDS
9conversion.
10
11\DESCRIBE
12{UNBETA_CONV t1 t2} returns a theorem of the form
13{
14   |- t2 = (\v. t') t1
15}
16The choice of {v} and the nature of {t'} depend on whether or {t1} is
17a variable.  If so, then {v} will be {t1} and {t'} will be {t2}.
18Otherwise, {v} will be generated with {genvar} and {t'} will be the
19result of substituting {v} for {t1}, wherever it occurs.
20
21\FAILURE
22Never fails.
23
24\COMMENTS
25Very useful for setting up a higher-order match by hand.  The use of
26{genvar} is predicated on the assumption that it will later be
27eliminated through the application of the function term to some other
28argument.
29
30\SEEALSO
31Thm.BETA_CONV
32
33\ENDDOC
34