Nuprl - DiscreteMath LEMMAs for card_split_sigma_dom

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

Rank	Theorem	Name
4	Thm* B:(AType), P:(AProp). Thm* (i:A. Dec(P(i))) Thm* Thm* ((i:AB(i)) ~ ((i:{i:A\| P(i) }B(i))+(i:{i:A\| P(i) }B(i))))	[card_split_sigma_dom_decbl]
cites the following:
1	Thm* B:(AType), P:(AProp). Thm* (i:{i:A\| P(i) }B(i)) ~ {v:(i:AB(i))\| P(v/x,y. x) }	[card_sigma_st_dom]
3	Thm* (x:A. Dec(P(x))) (A ~ ({x:A\| P(x) }+{x:A\| P(x) }))	[card_split_decbl]

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