Nuprl - mb_event_system_5 LEMMAs for ma_DASH_ds_DASH

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

Theorem	Name
Thm* M1,M2:MsgA, x:Id. M1 M2 (M2.ds(x) r M1.ds(x))	[ma-ds-sub]
cites the following:
Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g f (f(x)?T r g(x)?Top)	[subtype-fpf-cap-top]

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