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