----------------------------------------------------------------------
BINDER_CONV                                                     (Conv)
----------------------------------------------------------------------
BINDER_CONV : conv -> conv

SYNOPSIS
Applies a conversion underneath a binder.

KEYWORDS
conversion, quantifier.

DESCRIBE
If {conv N} returns {A |- N = P}, then {BINDER_CONV conv (M (\v.N))} returns
{A |- M (\v.N) = M (\v.P)} and {BINDER_CONV conv (\v.N)} returns
{A |- (\v.N) = (\v.P)}

FAILURE
If {conv N} fails, or if {v} is free in {A}.

EXAMPLE

- BINDER_CONV SYM_CONV (Term `\x. x + 0 = x`);
> val it = |- (\x. x + 0 = x) = \x. x = x + 0 : thm


COMMENTS
For deeply nested quantifiers, {STRIP_BINDER_CONV} and
{STRIP_QUANT_CONV} are more efficient than iterated application of
{BINDER_CONV}, {BINDER_CONV}, or {ABS_CONV}.

SEEALSO
Conv.QUANT_CONV, Conv.STRIP_QUANT_CONV, Conv.STRIP_BINDER_CONV,
Conv.ABS_CONV.

----------------------------------------------------------------------