Nuprl - mb_event_system_5 LEMMAs for ma_DASH_sub

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

Theorem	Name
Thm* M1,M2:MsgA. M1 M2 Prop{i'}	[ma-sub_wf]
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]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. f g (f(x)?Void r g(x)?T)	[subtype-fpf-cap-void]
Thm* B1,B2:(AType). Thm* (a:A. B1(a) r B2(a)) (a:A fp-> B1(a) r a:A fp-> B2(a))	[subtype-fpf2]

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