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

1

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

4 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html