DEPTH_EXISTS_CONV : (conv -> conv)
STRUCTURE
unwindLib
SYNOPSIS
Applies a conversion to the body of nested existential quantifications.
LIBRARY
unwind
DESCRIPTION
DEPTH_EXISTS_CONV conv "?x1 ... xn. body" applies conv to "body" and returns a theorem of the form: 
   |- (?x1 ... xn. body) = (?x1 ... xn. body')
FAILURE
Fails if the application of conv fails.
EXAMPLE
#DEPTH_EXISTS_CONV BETA_CONV "?x y z. (\w. x /\ y /\ z /\ w) T";;
|- (?x y z. (\w. x /\ y /\ z /\ w)T) = (?x y z. x /\ y /\ z /\ T)
SEEALSO
DEPTH_FORALL_CONV
HOL  Kananaskis-11