Since everything eventually becomes a `bool`, this operation could be implemented by translating
\\(\\phi(\\text{something_satisfying}(p), ...)\\) to \\(\\exists x. p x \\land \\phi(x, ...)\\)

This should be possible, but it would require some thought to implement correctly.
## Standard Library

Sure, this operation doesn't really return *a* number. But it's useful.

The basics:
```text
(+), (-), (*), (/) : number -> number -> number
(=), (<), (>), (<=), (>=) : number -> number -> bool
(&&), (||) : bool -> bool -> bool
(~) : bool -> bool
if : bool -> a -> a -> a
```

Useful derived functions:
```text
{-
    If you graph `x, y => y = x^2`, the result will be invisible, because it's an infinitely thin curve.
    If you graph `holds_within 0.1 (x, y => y = x^2)`, the result will be a curve of width 0.2, so you can actually see it.
-}
holds_within : number -> (number -> number -> bool) -> (number -> number -> bool)
holds_within r f x y = ∃x'. ∃y'. (x - x')^2 + (y - y')^2 <= r^2 && f x' y'
```

---