Object: ho_thm, theory combin
Display form: 'b,'c,'a:stype. (all (f:'b 'c. all (g:'a 'b. all (x:'a. equal (o f g x) (f (g x))))))
Term structure: all(stype; 'b.all(stype; 'c.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(hall('a); tlambda('a; x.apply(apply(hequal('c); apply(apply(apply(ho('b; 'c; 'a); f); g); x)); apply(f; apply(g; x)))))))))))))