Nuprl - mb_event_system_5 LEMMAs for fpf_DASH_compatible_DASH

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

Rank	Theorem	Name
5	Thm* eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). Thm* h \|\| f h \|\| g h \|\| f g	[fpf-compatible-join]
cites the following:
4	Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x dom(f g) f g(x) = if x dom(f) f(x) else g(x) fi B(x)	[fpf-join-ap]
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]

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