EXISTENCE : thm -> thm

SYNOPSIS
Deduces existence from unique existence.

DESCRIPTION
When applied to a theorem with a unique-existentially quantified conclusion, EXISTENCE returns the same theorem with normal existential quantification over the same variable.
    A |- ?!x. p
   -------------  EXISTENCE
    A |- ?x. p

FAILURE CONDITIONS
Fails unless the conclusion of the theorem is unique-existentially quantified.

EXAMPLE
  # let th = MESON[] `?!n. n = m`;;
  ...
  val th : thm = |- ?!n. n = m

  # EXISTENCE th;;
  val it : thm = |- ?n. n = m

SEE ALSO
EXISTS, SIMPLE_EXISTS.