theory Test type t
function f t t : t
clone algebra.AC with type t = t, function op = f, axiom .
goal G1 : forall x y : t. f x y = f y x
goal G2 : forall x y z : t. f (f x y) z = f x (f y z)
end
