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

1

4. x@0 : 'a 5. y : 'b 6. x = (a:'a. b:'b. (a = x@0)(b = y))  'a'b   x':hprod('a; 'b).    x = (a:'a. b:'b. (a = 1of(x'))(b = 2of(x')))  'a'bhbool

1 step

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