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