Object: hi_o_id, theory combin
Display form: 'b,'a:stype. (all (f:'a 'b. and (equal (o i f) f) (equal (o f i) f)))
Term structure: all(stype; 'b.all(stype; 'a.assert(apply(hall(hfun('a; 'b)); tlambda(hfun('a; 'b); f.apply(apply(hand; apply(apply(hequal(hfun('a; 'b)); apply(apply(ho('b; 'b; 'a); hi('b)); f)); f)); apply(apply(hequal(hfun('a; 'b)); apply(apply(ho('a; 'b; 'a); f); hi('a))); f)))))))