Nuprl - mb_event_system_5 LEMMAs for fpf_DASH_join

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

Rank	Theorem	Name
3	Thm* A:Type, B:(AType), f,g:a:A fp-> B(a), eq:EqDecider(A). Thm* f g a:A fp-> B(a)	[fpf-join_wf]
cites the following:
2	Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2)	[member_append]
2	Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x)	[member_filter]
2	Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L) (x L)	[assert-deq-member]

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