Nuprl - mb_event_system_6 LEMMAs for decidable__ex

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

Theorem	Name
Thm* P:(UnitProp). Dec(P()) Dec(x:Unit. P(x))	[decidable__ex_unit]
cites the following:
Thm* P:(TProp). (x:T. Dec(P(x))) finite-type(T) Dec(x:T. P(x))	[decidable-exists-finite]

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