x = new()

Example program we wish we can prove:

 x = new();
 y = new();
 assert (x != y);

Also:

assume (ALL n. next n != x);
y = new();
assert (ALL n. next n != x);

Solution:

x = new();

assume (x1 notin S);
x = x1;
S = S U {x1};

We obtain formulas with sets, in FOL eliminate them using quantifiers as in Deciding a language of sets and relations.