Object: hi_thm, theory combin
Display form: 'a:stype. (all (x:'a. equal (i x) x))
Term structure: all(stype; 'a.assert(apply(hall('a); tlambda('a; x.apply(apply(hequal('a); apply(hi('a); x)); x)))))