op a : bc

op a : b -> c

op a : s = e

op a :? s = e

ops __<__ : a * a -> b;

a : b -> c

op a :? b %(opbla)%

%(a)%

%(b)%

op a :? b %(op bla)%

%(a)%

%(b)%

op a : b -> c

op __<__ : a * a -> b

op a : b -> c

op a : b, assoc, comm, idem, assoc, unit 1, unit -, assoc

op a(a : b; a : b; a, b : c) :? b = e

ops a, bc, d, e : a ->? b, assoc, idem, comm

op a :? b

op e : a = e == e