Nuprl - mb_event_system_5 LEMMAs for fpf_DASH_single_DASH_sub_DASH

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

Theorem	Name
Thm* B:(AType), x:A, v:B(x), eqa:EqDecider(A). x : v x : v	[fpf-single-sub-reflexive]
cites the following:
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f = g f g	[fpf-sub_weakening]

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