EXISTS_DEL_CONV : conv
STRUCTURE
SYNOPSIS
Deletes existential quantifiers.
LIBRARY
unwind
DESCRIPTION
EXISTS_DEL_CONV "?x1 ... xn. t" returns the theorem:
   |- (?x1 ... xn. t) = t
provided x1,...,xn are not free in t.
FAILURE
Fails if any of the x’s appear free in t. The function does not perform a partial deletion; for example, if x1 and x2 do not appear free in t but x3 does, the function will fail; it will not return:
   |- ?x1 ... xn. t = ?x3 ... xn. t
SEEALSO
HOL  Trindemossen-1