For existential quantification, we use the `there-is` function.

Meanwhile, for universal quantification, we... just mention the variable. This intuitively makes sense: `there-is` is a restriction on a variable (the restriction is that there is at least one value for that variable). Meanwhile, the absence of restrictions implies universal quantification.

Specifying universal quantification like this is quite common in math proofs, and it's not too bad to get used to.