EXISTS_DEL1_CONV : conv
STRUCTURE
SYNOPSIS
Deletes one existential quantifier.
LIBRARY
unwind
DESCRIPTION
EXISTS_DEL1_CONV "?x. t" returns the theorem:
   |- (?x. t) = t
provided x is not free in t.
FAILURE
Fails if the argument term is not an existential quantification or if x is free in t.
SEEALSO
HOL  Kananaskis-13