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