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)

1	3. x' : hsum('a; 'b) 4. x'' : hsum('a; 'b) 5. rep_sum(x') = rep_sum(x'')  hbool'a'bhbool   x' = x''	1 step
2	3. x : hbool'a'bhbool 4. (f:'a'b. u:'a+'b. (f = (rep_sum(u))))(x)   x':hsum('a; 'b). x = rep_sum(x')  hbool'a'bhbool	1 step
3	3. x : hbool'a'bhbool 4. x':hsum('a; 'b). x = rep_sum(x')  hbool'a'bhbool   (f:'a'b. u:'a+'b. (f = (rep_sum(u))))(x)	1 step

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