Object: i_o_id, theory combin
Display form: 'b,'a:stype. x:'a 'b. (x:'b. x) o x = x x o (x:'a. x) = x
Term structure: all(stype; 'b.all(stype; 'a.all(hfun('a; 'b); x.and(equal(hfun('a; 'b); compose(tlambda('b; x.x); x); x); equal(hfun('a; 'b); compose(x; tlambda('a; x.x)); x)))))