Applies a consequence conversion to the body of an existentially
quantified term.
DESCRIPTION
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.