1. 'a : S
2. 'b : S
3. x : 'a'bhbool
4. is_pair(x)
  x':hprod('a; 'b). x = rep_prod(x')  'a'bhbool

1

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

2 steps

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