Thus, your formula is valid if x and y are declared as CONSTANTS, but not if at least one of them is a VARIABLE.
But in a system independant of TLAPLUS? For example if LTL is built upon FOL, the individual variables declared by FOL and that can be quantified are what: state variables or something else?