Object: hi_def, theory combin
Display form: 'a:stype. (equal i (s k k))
Term structure: all(stype; 'a.assert(apply(apply(hequal(hfun('a; 'a)); hi('a)); apply(apply(hs('a; hfun('a; 'a); 'a); hk('a; hfun('a; 'a))); hk('a; 'a)))))