QUANT_CONSEQ_CONV : (conseq_conv -> conseq_conv)
STRUCTURE
SYNOPSIS
Applies a consequence conversion to the body of an existentially or universally quantified term.
SEEALSO
HOL  Trindemossen-1