Exists(name: String, bound: Formula, target: Formula)
First-order exists operator. Specifies that there exists a state in bound, such that when substituted for name, the target formula is valid at the inspected state.
Note that (exists x in A : B) is semantically equivalent to (exists x : ((at x: A) && B)).
However, we allow the in syntax because it is much more readable and can yield interesting
performance optimisations.
Warning: name must usually be a free name (not assigned yet).