Def P  Q == (P  Q) & (P  Q)

is mentioned by

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]

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