Who Cites dstype?
dstype	Def dstype(TypeNames; d; a) == 1of(d)(a)
	Thm* TypeNames:Type, d:DS(TypeNames), a:TypeNames. Thm* dstype(TypeNames; d; a)  Type
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p)  A

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