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

1

6. x : 'a   f(x) = g(x)

1 step

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