Def SqStable(P) == P  P

is mentioned by

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]

In prior sections: core rel 1

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