No other cites to report in StandardLib
type_inj	Def [x]{T} == x
	Thm* T:Type, E:(TTProp). Thm* (EquivRel x,y:T. E(x,y))  (a:T. [a]{x,y:T//E(x,y)}  x,y:T//E(x,y))

Syntax:

[x]{T}

has structure:

type_inj(x; T)

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