some package:sbv

Choose a value that satisfies the given predicate. This is Hillbert's choice, essentially. Note that if the predicate given is not satisfiable (for instance const sFalse), then the element returned will be arbitrary. The only guarantee is that if there's at least one element that satisfies the predicate, then the returned element will be one of those that do. The returned element is not guaranteed to be unique, least, greatest etc, unless there happens to be exactly one satisfying element.