1. 'a : S
2. 'b : S
3. r : 'a'b
  (@u:'a+'b. (rep_sum(u) = r  'a'b))
  =
  (@a:'a+'b. (r = rep_sum(a)  'a'b))

By:	L Thm* T:S, P,Q:(TType). (x:T. P(x)  Q(x))  (@x:T. P(x)) = (@x:T. Q(x)) THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

None

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