----------------------------------------------------------------------
QUANT_CONV                                                      (Conv)
----------------------------------------------------------------------
QUANT_CONV : conv -> conv

SYNOPSIS
Applies a conversion underneath a quantifier.

KEYWORDS
conversion, quantifier.

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

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

EXAMPLE

- QUANT_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_QUANT_CONV} and {STRIP_BINDER_CONV}
are more efficient than iterated application of {QUANT_CONV}, {BINDER_CONV},
or {ABS_CONV}.

SEEALSO
Conv.BINDER_CONV, Conv.STRIP_QUANT_CONV, Conv.STRIP_BINDER_CONV,
Conv.ABS_CONV.

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