Def T == {:True| T }

is mentioned by

Thm* E:(TTProp).  Thm* (EquivRel x,y:T. E(x,y))  (a,b:T. a = b  x,y:T//E(x,y)  E(a,b))

[quot_elim]

In prior sections: core rel 1

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html