Object: hs_thm, theory combin
Display form: 'a,'b,'c:stype. (all (f:'a 'b 'c. all (g:'a 'b. all (x:'a. equal (s f g x) (f x (g x))))))
Term structure: all(stype; 'a.all(stype; 'b.all(stype; 'c.assert(apply(hall(hfun('a; hfun('b; 'c))); tlambda(hfun('a; 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(hs('a; 'b; 'c); f); g); x)); apply(apply(f; x); apply(g; x)))))))))))))