1. 'a : S
2. 'b : S
  (x',x'':'a+'b. rep_sum(x') = rep_sum(x'')  'a'b  x' = x'')
  & (x:('a'b). 
  & ((f:'a'b. u:'a+'b. (f = (rep_sum(u))))(x)
  & (
  & ((x':'a+'b. x = rep_sum(x')  'a'b))

1	x',x'':'a+'b. rep_sum(x') = rep_sum(x'')  'a'b  x' = x''	9 steps
2	x:('a'b).    (f:'a'b. u:'a+'b. (f = (rep_sum(u))))(x)      (x':'a+'b. x = rep_sum(x')  'a'b)	1 step

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