This part isn't explained very well on the web page, but each theorems we display on the web page each correspond to one part of a ".gh" file. In that file, we declare the variables, so x always represents a natural number within that file. (In fact in that file, the concept of integers, rationals, and real numbers isn't introduced until later, so all numbers are natural.)
Everything is very rigorously defined. The web page tries to put things in a human-readable format, so some of this isn't immediately obvious. There is a "notation help" button at the bottom of the theorem which helps explain what is going on here. The operation
(<*> x) is displayed as $x_1 * x_2 * ... x_n$. Here x is a finite sequence of numbers and (<*> x) is defined as the product of the numbers in the sequence. This finite sequence is represented as a tuple
. A tuple is defined in terms of ordered pairs. The tuple (A, B, C) is internally represented as (((A, B), C), 3). And then ordered pairs
are defined in terms of basic arithmetic using triangular numbers
. So we've been very careful here.