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)
8. abs_sum(rep_sum(u)) = u
9. abs_sum(rep_sum(v)) = v
  u = v

By:	ApplyFunToHypEquands (z:'a'b. abs_sum(z)) 5 THEN All Reduce THEN StrongAuto

1

10. abs_sum(rep_sum(u)) = abs_sum(rep_sum(v))   u = v

1 step

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