'b,'c,'a:S, x:('b  'c), x@0:('a  'b), x@1:'a.
  (x o x@0)(x@1) = x(x@0(x@1))

By:	RewriteOfThm Thm* 'b,'c,'a:S. Thm* all(f:'b  'c. all(g:'a  'b. all(x:'a. equal(o(f,g,x),f(g(x)))))) (SimpsetC [`hol_to_nuprl`])

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html