EXISTS_DEL1_CONV : conv
STRUCTURE
unwindLib
SYNOPSIS
Deletes one existential quantifier.
LIBRARY
unwind
DESCRIPTION
EXISTS_DEL1_CONV "?x. t"
returns the theorem:
|- (?x. t) = t
provided
x
is not free in
t
.
FAILURE
Fails if the argument term is not an existential quantification or if
x
is free in
t
.
SEEALSO
EXISTS_DEL_CONV
,
PRUNE_ONCE_CONV
HOL
Kananaskis-14