Object: ho_assoc, theory combin
Display form: 'a,'c,'d,'b:stype. (all (f:'c 'd. all (g:'b 'c. all (h:'a 'b. equal (o f (o g h)) (o (o f g) h)))))
Term structure: all(stype; 'a.all(stype; 'c.all(stype; 'd.all(stype; 'b.assert(apply(hall(hfun('c; 'd)); tlambda(hfun('c; 'd); f.apply(hall(hfun('b; 'c)); tlambda(hfun('b; 'c); g.apply(hall(hfun('a; 'b)); tlambda(hfun('a; 'b); h.apply(apply(hequal(hfun('a; 'd)); apply(apply(ho('c; 'd; 'a); f); apply(apply(ho('b; 'c; 'a); g); h))); apply(apply(ho('b; 'd; 'a); apply(apply(ho('c; 'd; 'b); f); g)); h)))))))))))))