1. 'a : S
2. 'b : S
3. x : 'a
4. y : 'b
  x@0:hprod('a; 'b). 
  (a:'a. b:'b. (a = 1of(x@0))(b = 2of(x@0)))
  = (a:'a. b:'b. (a = x)(b = y))

None

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