Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* E:(TTProp).  Thm* (EquivRel x,y:T. E(x,y)) Thm*  Thm* (x,y:T. Dec(E(x,y)))  (u,v:x,y:T//E(x,y). Dec(u = v))	[decidable__quotient_equal]
Thm* E:(TTProp).  Thm* (x,y:T. Dec(E(x,y)))  (f:(TT). x,y:T. (x f y)  E(x,y))	[dec_iff_ex_bvfun]
Thm* E:(TTProp).  Thm* (EquivRel x,y:T. E(x,y)) Thm*  Thm* (F:((x,y:T//E(x,y))Prop).  Thm* ((w:x,y:T//E(x,y). SqStable(F(w))) Thm* ( Thm* (((z:x,y:T//E(x,y). F(z))  (z:T. F(z))))	[all_quot_elim]
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]
Thm* E:(TTProp). (EquivRel x,y:T. E(x,y))  T  (x,y:T//E(x,y))	[quotient_qinc]
Thm* T:Type, E:(TTProp). (EquivRel x,y:T. E(x,y))  x,y:T//E(x,y)  Type	[quotient_wf]

In prior sections: core well fnd int 1 bool 1 rel 1

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