Some definitions of interest.
d-sub	Def D1  D2 == i:Id. M(i)  M(i)
dsys	Def Dsys == IdMsgA
	Thm* Dsys  Type{i'}

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