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