Nuprl - DiscreteMath LEMMAs for card_sigma_vs_nsub

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

Rank	Theorem	Name
7	Thm* a:, b:(a). (i:ab(i)) ~ ( i:a. b(i))	[card_sigma_vs_nsub_sigma]
cites the following:
0	Thm* (A ~ 0) (A)	[card0_iff_uninhabited]
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]
1	Thm* f:(AAA), u:A, a,b:, e:({a..b}A). Thm* a<b (Iter(f;u) i:{a..b}. e(i)) = f(Iter(f;u) i:{a..b-1}. e(i),e(b-1))	[iter_via_intseg_split_last]
3	Thm* a,a':. a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a))	[card_sum_family_intseg_singleton_elim]
6	Thm* a,b:. (a+b) ~ (a+b)	[nsub_add_rw]

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