We can define an auxiliary fresh function f
from S
to Int
, and assert
f(a_1) = 1
f(a_1) = 2
f(a_3) = 3
...
f(a_n) = n
Then, a_1
, ..., a_n
must be different from each other.
If we want to say that b
is also different from all a_i
s. We just assert
f(b) = n+1
In this approach, we only have to track the counter.