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