Object: hk_wf, theory combin
Display form: 'a,'b:stype. k 'a 'b 'a
Term structure: all(stype; 'a.all(stype; 'b.member(hfun('a; hfun('b; 'a)); hk('a; 'b))))