NOT_EXISTS_CONV : conv

- STRUCTURE
- SYNOPSIS
- Moves negation inwards through an existential quantification.
- DESCRIPTION
- When applied to a term of the form ~(?x.P), the conversion NOT_EXISTS_CONV returns the theorem:
|- ~(?x.P) = !x.~P

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

HOL Kananaskis-14