UNBETA_CONVConv.UNBETA_CONV : term -> convReturns a reversed instance of beta-reduction.
UNBETA_CONV t1 t2 returns a theorem of the form
|- t2 = (\v. t') t1The 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.
Never fails.
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.