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.