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(T), f,g,h:x:T fp-> Type. Thm* f \|\| g Thm* Thm* h \|\| f Thm* Thm* h \|\| g Thm* Thm* g h f g & f h f g & h g h f g & h f h f g	[fpf-compatible-triple]
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* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A. Thm* f g(x) ~ if x dom(f) f(x) else g(x) fi	[fpf-join-ap-sq]

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