Nuprl - DiscreteMath LEMMAs for card_pi_vs_nsub

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

Rank	Theorem	Name
9	Thm* a:, b:(a). (i:ab(i)) ~ ( i:a. b(i))	[card_pi_vs_nsub_pi]
cites the following:
0	Thm* (A ~ 1) (!A)	[card1_iff_inhabited_uniquely]
3	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_prod_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]
2	Thm* a,a':. a'-a = 1 (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a))	[card_prod_family_intseg_singleton_elim]
8	Thm* a,b:. (ab) ~ (ab)	[nsub_mul_rw]
1	Thm* a,b:. 0ab	[mul_bounds_1a]

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