QUANT_CONV
Conv.QUANT_CONV : conv -> conv
Applies a conversion underneath a quantifier.
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.
See also
Conv.BINDER_CONV,
Conv.STRIP_QUANT_CONV,
Conv.STRIP_BINDER_CONV,
Conv.ABS_CONV