'a,'b:S.
  exists
  (rep:hsum('a; 'b)  hbool  'a  'b  hbool. type_definition
  (rep:hsum('a; 'b)  hbool  'a  'b  hbool. (is_sum_rep
  (rep:hsum('a; 'b)  hbool  'a  'b  hbool. ,rep))

1

1. 'a : S 2. 'b : S   rep:(hsum('a; 'b)hbool'a'bhbool).    type_definition(hbool'a'bhbool;hsum('a; 'b);is_sum_rep;rep)

4 steps

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