1. 'a : S
2. 'b : S
3. u : 'a+'b
4. v : 'a+'b
5. rep_sum(u) = rep_sum(v)
6. a:hsum('a; 'b). abs_sum(rep_sum(a)) = a
7. r:(hbool  'a  'b  hbool). is_sum_rep(r) = ((rep_sum(abs_sum(r))) = r)
  u = v

1

8. abs_sum(rep_sum(u)) = u  hsum('a; 'b) 9. abs_sum(rep_sum(v)) = v  hsum('a; 'b)   u = v

2 steps

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