'a,'b:S.
  all
  (x:'a. all
  (x:'a. (y:'b. equal
  (x:'a. (y:'b. (mk_pair(x,y)
  (x:'a. (y:'b. ,a:'a. b:'b. and(equal(a,x),equal(b,y)))))

1

1. 'a : S 2. 'b : S 3. x : 'a 4. y : 'b   mk_pair(x,y) = (a:'a. b:'b. (a = x)(b = y))  ('a  'b  hbool)

1 step

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html