'a,'b:S.
  (p:'a'b. a:'a. b:'b. (a = 1of(p))(b = 2of(p)))
  =
  (@rep:'a'b'a'b
  (@((p',p'':'a'b.  ((rep(p')) = (rep(p'')))(p' = p''))
  (@(x:'a'b
  (@(((his_pair('a; 'b)(x)) = (p':'a'b. (x = (rep(p'))))))))

None

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