NOT_PEXISTS_CONV
PairRules.NOT_PEXISTS_CONV : conv
Moves negation inwards through a paired existential quantification.
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).
See also
Conv.NOT_EXISTS_CONV,
PairRules.PEXISTS_NOT_CONV,
PairRules.PFORALL_NOT_CONV,
PairRules.NOT_PFORALL_CONV