Nuprl - mb_event_system_5 LEMMAs for fpf_DASH_sub

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

Rank	Theorem	Name
6	Thm* strong-subtype(A;A') Thm* Thm* (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), Thm* (f,g:a:A fp-> B(a). (a:A. B(a) r C(a)) f g f g)	[fpf-sub_functionality]
cites the following:
5	Thm* strong-subtype(A;A') Thm* Thm* (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), Thm* (f,g:a:A fp-> B(a). (a:A. B(a) r C(a)) f g f g)	[fpf-sub-functionality]

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