1\DOC DEPTH_EXISTS_CONV
2
3\TYPE {DEPTH_EXISTS_CONV : (conv -> conv)}
4
5\SYNOPSIS
6Applies a conversion to the body of nested existential quantifications.
7
8\LIBRARY unwind
9
10\DESCRIBE
11{DEPTH_EXISTS_CONV conv "?x1 ... xn. body"} applies {conv} to {"body"} and
12returns a theorem of the form:
13{
14   |- (?x1 ... xn. body) = (?x1 ... xn. body')
15}
16
17\FAILURE
18Fails if the application of {conv} fails.
19
20\EXAMPLE
21{
22#DEPTH_EXISTS_CONV BETA_CONV "?x y z. (\w. x /\ y /\ z /\ w) T";;
23|- (?x y z. (\w. x /\ y /\ z /\ w)T) = (?x y z. x /\ y /\ z /\ T)
24}
25\SEEALSO
26unwindLib.DEPTH_FORALL_CONV.
27
28\ENDDOC
29