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.