Convert a theorem representing a single-line definition into a fully
lambda-abstracted version.
DESCRIPTION
Given a theorem which describes an equation for a constant applied to a series
of distinct variables, derive a reformulation which equates the constant with a
lambda-abstraction over those variables.
USES
To advance a proof by unfolding a partially-applied function. Most effectively
used on theorems produced by oneline.
EXAMPLE
Consider the result of applying oneline to listTheory.MAP:
> oneline listTheory.MAP;
val it = ⊢ MAP f v = case v of [] => [] | h::t => f h::MAP f t: thm
> lambdify it;
val it = ⊢ MAP = (λf v. case v of [] => [] | h::t => f h::MAP f t): thm
FAILURE
Fails on theorems of the wrong form, i.e. theorems which are not a single
equation with a left-hand side consisting of an application to a series of
distinct variables.