Eliminate lambda-terms that are not part of quantifiers from Boolean term.
DESCRIPTION
When applied to a Boolean term, LAMBDA_ELIM_CONV returns an equivalent
version with `bare' lambda-terms (those not part of quantifiers) removed. They
are replaced with new `function' variables and suitable hypotheses about them;
for example a lambda-term \x. t[x] is replaced by a function f with an
additional hypothesis !x. f x = t[x].
FAILURE CONDITIONS
Never fails.
EXAMPLE
# LAMBDA_ELIM_CONV `MAP (\x. x + 1) l = l'`;;
val it : thm =
|- MAP (\x. x + 1) l = l' <=>
(!_73141. (!x. _73141 x = x + 1) ==> MAP _73141 l = l')
USES
This is mostly intended for normalization prior to automated proof procedures,
and is used by MESON, for example. However, it may sometimes be useful in
itself.