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