Object: hk_thm, theory combin
Display form: 'a,'b:stype. (all (x:'a. all (y:'b. equal (k x y) x)))
Term structure: all(stype; 'a.all(stype; 'b.assert(apply(hall('a); tlambda('a; x.apply(hall('b); tlambda('b; y.apply(apply(hequal('a); apply(apply(hk('a; 'b); x); y)); x))))))))