Nuprl - DiscreteMath LEMMAs for card_split_end_sum_intseg

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

Rank	Theorem	Name
6	Thm* a,b:, B:({a..b}Type). Thm* a<b ((i:{a..b}B(i)) ~ ((i:{a..(b-1)}B(i))+B(b-1)))	[card_split_end_sum_intseg_family]
cites the following:
5	Thm* a,b:, c:{a...b}, B:({a..b}Type). Thm* (i:{a..b}B(i)) ~ ((i:{a..c}B(i))+(i:{c..b}B(i)))	[card_split_sum_intseg_family]
0	Thm* (A ~ A') (B ~ B') ((A+B) ~ (A'+B'))	[union_functionality_wrt_one_one_corr]
3	Thm* a,a':. a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a))	[card_sum_family_intseg_singleton_elim]

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