NOT_PEXISTS_CONV : conv
STRUCTURE
PairRules
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
NOT_EXISTS_CONV, PEXISTS_NOT_CONV, PFORALL_NOT_CONV, NOT_PFORALL_CONV
HOL  Trindemossen-1