Nuprl - mb_event_system_1 LEMMAs for finite_DASH_decidable_DASH

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

Rank	Theorem	Name
5	Thm* P:(TProp). Thm* (x:T. Dec(P(x))) Thm* Thm* (finite-type({x:T\| P(x) }) (L:T List. x:T. P(x) (x L)))	[finite-decidable-set]
cites the following:
4	Thm* P:(TProp). Thm* (x:T. SqStable(P(x))) Thm* Thm* (finite-type({x:T\| P(x) }) (L:T List. x:T. P(x) (x L)))	[finite-set-type]
2	Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x)	[member_filter]

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