NOT_PFORALL_CONV : conv
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Moves negation inwards through a paired universal quantification.
DESCRIPTION
When applied to a term of the form ~(!p. t), the conversion NOT_PFORALL_CONV returns the theorem: 
   |- ~(!p. t) = (?p. ~t)
It is irrelevant whether any variables in p occur free in t.
FAILURE
Fails if applied to a term not of the form ~(!p. t).
SEEALSO
NOT_FORALL_CONV, PEXISTS_NOT_CONV, PFORALL_NOT_CONV, NOT_PEXISTS_CONV
HOL  Trindemossen-1