Object: o_assoc, theory combin
Display form: 'a,'c,'d,'b:stype. x:'c 'd. x@0:'b 'c. x@1:'a 'b. x o (x@0 o x@1) = (x o x@0) o x@1
Term structure: all(stype; 'a.all(stype; 'c.all(stype; 'd.all(stype; 'b.all(hfun('c; 'd); x.all(hfun('b; 'c); x@0.all(hfun('a; 'b); x@1.equal(hfun('a; 'd); compose(x; compose(x@0; x@1)); compose(compose(x; x@0); x@1)))))))))