1. 'a : S
2. 'b : S
3. f : hbool  'a  'b  hbool
4. y : 'b
5. f = (b:. x:'a. y@0:'b. (y@0 = y)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