NOT_FORALL_CONV : conv

- STRUCTURE
- SYNOPSIS
- Moves negation inwards through a universal quantification.
- DESCRIPTION
- When applied to a term of the form ~(!x.P), the conversion NOT_FORALL_CONV returns the theorem:It is irrelevant whether x occurs free in P.
|- ~(!x.P) = ?x.~P

- FAILURE
- Fails if applied to a term not of the form ~(!x.P).
- SEEALSO

HOL Kananaskis-14