Object: hi_wf, theory combin
Display form: 'a:stype. i 'a 'a
Term structure: all(stype; 'a.member(hfun('a; 'a); hi('a)))