Object: i_thm, theory combin
Display form: 'a:stype. x:'a. x = x
Term structure: all(stype; 'a.all('a; x.equal('a; x; x)))