Object: ho_wf, theory combin
Display form: 'b,'c,'a:stype. o ('b 'c) ('a 'b) 'a 'c
Term structure: all(stype; 'b.all(stype; 'c.all(stype; 'a.member(hfun(hfun('b; 'c); hfun(hfun('a; 'b); hfun('a; 'c))); ho('b; 'c; 'a)))))