sort a, b, c
pred q:a; p : a
pred q,p:b
op o : a -> b
op o2 : a ->? b
sort a < d
op o : a , assoc
var c : a
. o(c) = o2(c)
sort x = { y:a . y = c}