Nuprl - hol_sum LEMMAs for hinr

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

Rank	Theorem	Name
4	Thm* 'a,'b:S. Thm* all Thm* (e:'b. equal Thm* (e:'b. (inr(e) Thm* (e:'b. ,abs_sum(b:hbool. x:'a. y:'b. and(equal(y,e),not(b)))))	[hinr_def]
cites the following:
3	Thm* 'a,'b:S. Thm* (x:'a+'b. abs_sum(rep_sum(x)) = x 'a+'b) Thm* & (x:('a'b). is_sum_rep(x) = ((rep_sum(abs_sum(x))) = x))	[sum_iso]

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