----------------------------------------------------------------------
EXISTS_CONSEQ_CONV                                        (ConseqConv)
----------------------------------------------------------------------
EXISTS_CONSEQ_CONV : (conseq_conv -> conseq_conv)

SYNOPSIS
Applies a consequence conversion to the body of an existentially
quantified term.

DESCRIBE
If {c} is a consequence conversion that maps a term {``t x``}
to a theorem {|- t x = t' x},  {|- t' x ==> t x} or
{|- t x ==> t' x}, then {EXISTS_CONSEQ_CONV c} maps {``?x. t x``} to
{|- ?x. t x = ?x. t' x},  {|- ?x. t' x ==> ?x. t x} or
{|- ?x. t x ==> ?x. t' x}, respectively.

FAILURE
{EXISTS_CONSEQ_CONV c t} fails, if {t} is not an existentially
quantified term or if {c} fails on the body of {t}.

SEEALSO
Conv.QUANT_CONV, ConseqConv.FORALL_CONSEQ_CONV,
ConseqConv.QUANT_CONSEQ_CONV.

----------------------------------------------------------------------