'a,'b:S.
  all
  (p:hprod('a; 'b). equal
  (p:hprod('a; 'b). (snd(p)
  (p:hprod('a; 'b). ,select
  (p:hprod('a; 'b). ,(y:'b. exists(x:'a. equal(mk_pair(x,y),rep_prod(p))))))

1

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

4 steps

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