Nuprl - mb_event_system_5 LEMMAs for fpf_DASH_sub_DASH_join_DASH

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

Rank	Theorem	Name
5	Thm* B1,B2:(AType), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a). Thm* f f g	[fpf-sub-join-left]
cites the following:
4	Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A. Thm* x dom(f g) x dom(f) x dom(g)	[fpf-join-dom2]
0	Thm* B,C:(AType), eq:EqDecider(A), f:a:A fp-> B(a), g:a:A fp-> C(a), x:A. Thm* x dom(f) f g(x) = f(x) B(x)	[fpf-join-ap-left]

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