NOT_PFORALL_CONV : conv
STRUCTURE
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
HOL  Trindemossen-1