'c,'b,'a:S. all(f:'b  'c. all(g:'a  'b. equal(o(f,g),x:'a. f(g(x)))))

1

1. 'c : S 2. 'b : S 3. 'a : S 4. f : 'b'c 5. g : 'a'b   f o g = (x:'a. f(g(x)))

1 step

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