sort s, t;
ops a, o : s
. a = o
. def o %implied