defun-sk, may be
preferable.
Major Section: DEFUN-SK
The symbol exists (in the ACL2 package) represents existential
quantification in the context of a defun-sk form.
See defun-sk and see forall.
See quantifiers for an example illustrating how the use of
recursion, rather than explicit quantification with defun-sk, may be
preferable.