Object: hs_wf, theory combin
Display form: 'a,'b,'c:stype. s ('a 'b 'c) ('a 'b) 'a 'c
Term structure: all(stype; 'a.all(stype; 'b.all(stype; 'c.member(hfun(hfun('a; hfun('b; 'c)); hfun(hfun('a; 'b); hfun('a; 'c))); hs('a; 'b; 'c)))))