Nuprl - DiscreteMath LEMMAs for ifthenelse_distr_subtype

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

Theorem	Name
Thm* {x:A\| if b P(x) else Q(x) fi } ~ if b {x:A\| P(x) } else {x:A\| Q(x) } fi	[ifthenelse_distr_subtype_ooc]
cites the following:
Thm* {x:A\| if b P(x) else Q(x) fi } Thm* =ext Thm* if b {x:A\| P(x) } else {x:A\| Q(x) } fi	[ifthenelse_distr_subtype]

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