Object: s_thm, theory combin
Display form: 'a,'b,'c:stype. x:'a 'b 'c. x@0:'a 'b. x@1:'a. x x@1 (x@0 x@1) = x x@1 (x@0 x@1)
Term structure: all(stype; 'a.all(stype; 'b.all(stype; 'c.all(hfun('a; hfun('b; 'c)); x.all(hfun('a; 'b); x@0.all('a; x@1.equal('c; apply(apply(x; x@1); apply(x@0; x@1)); apply(apply(x; x@1); apply(x@0; x@1)))))))))