1. 'b : S
2. 'a : S
  (f:'a'b. e:'a. let x = e in f(x)) = (f:'a'b. x:'a. f(x))

1

(f:'a'b. e:'a. let x = e in f(x)) = (f:'a'b. x:'a. f(x))

1 step

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