Def S  T == x:S. x  T

is mentioned by

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

[quotient_qinc]

In prior sections: int 1

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