Nuprl - mb_event_system_5 LEMMAs for fpf_DASH_sub_DASH

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

Rank	Theorem	Name
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]
cites the following:
4	Thm* eq:EqDecider(Y), f:x:X fp-> Top, x:Y. Thm* strong-subtype(X;Y) x dom(f) x X	[fpf-dom-type2]
1	Thm* strong-subtype(A;B) (EqDecider(B) r EqDecider(A))	[strong-subtype-deq-subtype]
4	Thm* eq1,eq2:EqDecider(A), f:a:A fp-> Top, x:A. x dom(f) x dom(f)	[fpf-dom_functionality2]
2	Thm* B1:(A1Type), B2:(A2Type). Thm* strong-subtype(A1;A2) Thm* Thm* (a:A1. B1(a) r B2(a)) (a:A1 fp-> B1(a) r a:A2 fp-> B2(a))	[subtype-fpf3]

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