Nuprl - mb_event_system_4 LEMMAs for fpf_DASH_join_DASH

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

Rank	Theorem	Name
3	Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x dom(f g) x dom(f) x dom(g)	[fpf-join-dom]
cites the following:
2	Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x)	[member_filter]
2	Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2)	[member_append]
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