NOT_PEXISTS_CONV : conv
STRUCTURE
LIBRARY
pair
SYNOPSIS
Moves negation inwards through a paired existential quantification.
DESCRIPTION
When applied to a term of the form ~(?p. t), the conversion NOT_PEXISTS_CONV returns the theorem:
   |- ~(?p. t) = (!p. ~t)

FAILURE
Fails if applied to a term not of the form ~(?p. t).
SEEALSO
HOL  Trindemossen-1