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