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