QUANT_CONSEQ_CONV
ConseqConv.QUANT_CONSEQ_CONV : (conseq_conv -> conseq_conv)
Applies a consequence conversion to the body of an existentially or universally quantified term.
See also
Conv.QUANT_CONV,
ConseqConv.FORALL_CONSEQ_CONV,
ConseqConv.EXISTS_CONSEQ_CONV