(4steps total) PrintForm Definitions Lemmas hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hinr def 1 1
1. 'a : S
2. 'b : S
3. e : 'b
  inr(e) = abs_sum(rep_sum(inr(e)))  'a+'b
By: SwapEquands 0 THEN L Thm: sum iso THEN StrongAuto

Generated subgoals:

None

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

(4steps total) PrintForm Definitions Lemmas hol sum Sections HOLlib Doc