Nuprl - hol_sum LEMMAs for hsum_ty

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

Rank	Theorem	Name
4	Thm* 'a,'b:S. Thm* exists Thm* (rep:hsum('a; 'b) hbool 'a 'b hbool. type_definition Thm* (rep:hsum('a; 'b) hbool 'a 'b hbool. (is_sum_rep Thm* (rep:hsum('a; 'b) hbool 'a 'b hbool. ,rep))	[hsum_ty_def]
cites the following:
3	Thm* 'a,'b:S, u,v:'a+'b. rep_sum(u) = rep_sum(v) 'a'b u = v	[hrep_sum_inj]

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