1. 'a : S
2. 'b : S
3. f : hbool  'a  'b  hbool
4. x : 'a
5. f = (b:. x@0:'a. y:'b. (x@0 = x)b)
  v1:'a, v2:'b.
  f = (b:hbool. x:'a. y:'b. (x = v1)b)  (hbool  'a  'b  hbool)
   f
   =
   (b:hbool. x@0:'a. y:'b. (y = v2)b)
    (hbool  'a  'b  hbool)

None

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