'a,'b:S.
  exists(rep:hprod('a; 'b)  'a  'b  hbool. type_definition(is_pair,rep))

1

1. 'a : S 2. 'b : S   rep:(hprod('a; 'b)'a'bhbool).    type_definition('a'bhbool;hprod('a; 'b);is_pair;rep)

9 steps

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