spec s1 =
sort s, t;
ops a, o : s
. a = o
. o = a %implied
spec s2 = s1 then
sort u, v
then
preds p, q : s * v
. forall x : v . p(a, x)