Nuprl - hol_sum LEMMAs for sum

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

Theorem	Name
Thm* 'c,'b,'a:S, f:('a'c), g:('b'c). Thm* (h:(('a+'b)'c). Thm* (h o (x:'a. inl(x)) = f 'a'c & h o (x:'b. inr(x)) = g 'b'c) Thm* & (h,y:(('a+'b)'c). Thm* & (h o (x:'a. inl(x)) = f 'a'c & h o (x:'b. inr(x)) = g 'b'c Thm* & (& y o (x:'a. inl(x)) = f 'a'c Thm* & (& y o (x:'b. inr(x)) = g 'b'c Thm* & ( Thm* & (h = y)	[sum_axiom]
cites the following:
Thm* 'c,'b,'a:S. Thm* all Thm* (f:'a 'c. all Thm* (f:'a 'c. (g:'b 'c. exists_unique Thm* (f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. and Thm* (f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. (equal(o(h,inl),f) Thm* (f:'a 'c. (g:'b 'c. (h:hsum('a; 'b) 'c. ,equal(o(h,inr),g)))))	[hsum_axiom]

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