Words $w$ and $w'$ that interpret all variables in the same way satisfy the same set o f formulas: if for all $i$, $1\leq i \leq K$,The ShortTalk command save term tair, with the mouse over the beginning of $1\leq..., does not recognize the whole expression $1\leq i \leq K$.